cispa_all_3338.pdf (383.26 kB)

Securing Asynchronous Exceptions

Download (383.26 kB)
conference contribution
posted on 2023-11-29, 18:14 authored by Carlos Tomé Cortiñas, Marco Vassena, Alejandro Russo
Language-based information-flow control (IFC) techniques often rely on special purpose, ad-hoc primitives to address different covert channels that originate in the runtime system, beyond the scope of language constructs. Since these piecemeal solutions may not compose securely, there is a need for a unified mechanism to control covert channels. As a first step towards this goal, we argue for the design of a general interface that allows programs to safely interact with the runtime system and the available computing resources. To coordinate the communication between programs and the runtime system, we propose the use of asynchronous exceptions (interrupts), which, to the best of our knowledge, have not been considered before in the context of IFC languages. Since asynchronous exceptions can be raised at any point during execution—often due to the occurrence of an external event—threads must temporarily mask them out when manipulating locks and shared data structures to avoid deadlocks and, therefore, breaking program invariants. Crucially, the naive combination of asynchronous exceptions with existing features of IFC languages (e.g., concurrency and synchronization variables) may open up new possibilities of information leakage. In this paper, we present MACasync, a concurrent, statically enforced IFC language that, as a novelty, features asynchronous exceptions. We show how asynchronous exceptions easily enable (out of the box) useful programming patterns like speculative ex- ecution and some degree of resource management. We prove that programs in MACasync satisfy progress-sensitive non-interference and mechanize our formal claims in the Agda proof assistant.


Preferred Citation

Carlos Cortiñas, Marco Vassena and Alejandro Russo. Securing Asynchronous Exceptions. In: IEEE Computer Security Foundations Symposium (CSF). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

IEEE Computer Security Foundations Symposium (CSF)

Legacy Posted Date


Open Access Type

  • Unknown


@inproceedings{cispa_all_3338, title = "Securing Asynchronous Exceptions", author = "Cortiñas, Carlos Tomé and Vassena, Marco and Russo, Alejandro", booktitle="{IEEE Computer Security Foundations Symposium (CSF)}", year="2020", }

Usage metrics


    No categories selected


    Ref. manager