CISPA
Browse
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.

History

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

2021-01-07

Open Access Type

  • Unknown

BibTeX

@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

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC