Securing Verified IO Programs Against Unverified Code in F* - INRIA Chile
Journal Articles Proceedings of the ACM on Programming Languages Year : 2024

Securing Verified IO Programs Against Unverified Code in F*

Abstract

We introduce SCIO*, a formally secure compilation framework for statically verified programs performing input-output (IO). The source language is an F* subset in which a verified program interacts with its IO-performing context via a higher-order interface that includes refinement types as well as pre- and post-conditions about past IO events. The target language is a smaller F* subset in which the compiled program is linked with an adversarial context that has an interface without refinement types, pre-conditions, or concrete post-conditions. To bridge this interface gap and make compilation and linking secure we propose a formally verified combination of higher-order contracts and reference monitoring for recording and controlling IO operations. Compilation uses contracts to convert the logical assumptions the program makes about the context into dynamic checks on each context-program boundary crossing. These boundary checks can depend on information about past IO events stored in the state of the monitor. But these checks cannot stop the adversarial target context before it performs dangerous IO operations. Therefore linking in SCIO* additionally forces the context to perform all IO actions via a secure IO library, which uses reference monitoring to dynamically enforce an access control policy before each IO operation. We prove in F* that SCIO* soundly enforces a global trace property for the compiled verified program linked with the untrusted context. Moreover, we prove in F* that SCIO* satisfies by construction Robust Relational Hyperproperty Preservation, a very strong secure compilation criterion. Finally, we illustrate SCIO* at work on a simple web server example.
Fichier principal
Vignette du fichier
2303.01350.pdf (895.84 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04484770 , version 1 (29-02-2024)

Identifiers

Cite

Cezar-Constantin Andrici, Ștefan Ciobâcă, Cătălin Hriţcu, Guido Martínez, Exequiel Rivas, et al.. Securing Verified IO Programs Against Unverified Code in F*. Proceedings of the ACM on Programming Languages, 2024, 8 (POPL), pp.2226-2259. ⟨10.1145/3632916⟩. ⟨hal-04484770⟩
171 View
55 Download

Altmetric

Share

More