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.

Compiler correctness, in its simplest form, is defined as the inclusion of the set of traces of the compiled program in the set of traces of the original program. This is equivalent to the preservation of all trace properties. Here, traces collect, for instance, the externally observable events of each execution. However, this definition requires the set of traces of the source and target languages to be the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many definitions of secure compilation, which characterize the protection of a compiled program linked against adversarial code.

Abstract Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show in order to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side-channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many secure compilation definitions, which characterize the protection of a compiled program against linked adversarial code.

This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language. The soundness has also been mechanized in Coq. This approach is implemented in a tool for semantics-based verification as part of the K framework (http://kframework.org)

Abstract Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for full equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: a proof tree establishes the full equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known whether the sequence terminates or not; nevertheless, our proof system shows that the two programs are fully equivalent (even if we cannot establish termination or divergence of either one).

Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality, and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryptographic protocols. As in the applied pi calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory that allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence, which can therefore be automatically verified for such processes. When protocols are not determinate, our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those whose equational theory is generated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool Active Knowledge in Security Protocols and has been effectively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.

This paper introduces (one-path) reachability logic, a language-independent proof system for program verification, which takes an operational semantics as axioms and derives reachability rules, which generalize Hoare triples. This system improves on previous work by allowing operational semantics given with conditional rewrite rules, which are known to support all major styles of operational semantics. In particular, Kahn's big-step and Plotkin's small-step semantic styles are now supported. The reachability logic proof system is shown sound (i.e., partially correct) and (relatively) complete. Reachability logic thus eliminates the need to independently define an axiomatic and an operational semantics for each language, and the nonnegligible effort to prove the former sound and complete w.r.t. the latter. The soundness result has also been formalized in Coq, allowing reachability logic derivations to serve as formal proof certificates that rely only on the operational semantics.

We study the composition of security protocols when protocols share secrets such as keys. We show (in a Dolev-Yao model) that if two protocols use disjoint cryptographic primitives, their composition is secure if the individual protocols are secure, even if they share data. Our result holds for any cryptographic primitives that can be modeled using equational theories, such as encryption, signature, MAC, exclusive-or, and Diffie-Hellman. Our main result transforms any attack trace of the combined protocol into an attack trace of one of the individual protocols. This allows various ways of combining protocols such as sequentially or in parallel, possibly with inner replications. As an application, we show that a protocol using preestablished keys may use any (secure) key-exchange protocol without jeopardizing its security, provided that they do not use the same primitives. This allows us, for example, to securely compose a Diffie-Hellman key exchange protocol with any other protocol using the exchanged key, provided that the second protocol does not use the Diffie-Hellman primitives. We also explore tagging, which is a way of forcing the disjointness of two protocols that share cryptographic primitives We explain why composing protocols which use tagged cryptographic primitives like encryption and hash functions is secure by reducing this problem to the previous one.