View publication

Title Securing Verified IO Programs Against Unverified Code in F*
Authors Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Theo Winterhalter
Publication date January 2024
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.
Downloaded 81 times
Pages 2226-2259
Volume 8
Journal name Proceedings of the ACM Programming Languages
Publisher ACM Press (New York, NY, USA)
Reference URL View reference page