Cezar Andrici on Securing Verified IO Programs Against Unverified Code in F*
7 views
Skip to first unread message
Nikhil Swamy
Jul 23, 2023, 5:36:23 PM7/23/23
to fstar-mai...@googlegroups.com
On Tuesday, July 25th at 830am PDT, we have our next PoP Up Seminar.
Looking forward to seeing you there!
-Nik
Speaker
Cezar Andrici
Title
Securing Verified IO Programs Against Unverified Code in F*
Abstract
We introduce a formally secure compilation framework for statically
verified partial 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 via an interface without
refinement types or pre- and 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 our
linking process 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 enforcing the access control policy on the context
in combination with static verification of the program soundly enforces
a global trace property. Moreover, we prove in F* that our secure
compilation framework satisfies by construction Robust Relational
Hyperproperty Preservation, a very strong secure compilation criterion.
Finally, we illustrate our secure compilation framework at work on a
simple web server example.
Reply all
Reply to author
Forward
0 new messages