Verifying that a compiler preserves concurrent value-dependent information-flow security
Robert Sison (Data61, CSIRO, UNSW Sydney), Toby Murray (University, of Melbourne)
TL;DR
This paper introduces a decomposition principle for verifying that compilers preserve value-dependent information-flow security in concurrent programs, demonstrated through formal proof and application to a real compiler in Isabelle/HOL.
Contribution
It provides a new decomposition method that simplifies proving security preservation in compiler verification for concurrent, value-dependent security properties.
Findings
Decomposition principle reduces proof complexity by nearly half.
Successfully verified security preservation in a compiler from a While language to RISC assembly.
Applied verification to a real-world concurrent program model, demonstrating practical impact.
Abstract
It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency. Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Data61, CSIRO, Australia and UNSW Sydney, Australia [email protected]://orcid.org/0000-0003-0313-9764Australian Government RTP Scholarship & Data61 Research Project AwardUniversity of Melbourne, [email protected]\CopyrightRobert Sison and Toby Murray{CCSXML} <ccs2012> <concept> <concept_id>10002978.10002986.10002990</concept_id> <concept_desc>Security and privacy Logic and verification</concept_desc> <concept_significance>500</concept_significance> </concept> <concept> <concept_id>10002978.10003006.10011608</concept_id> <concept_desc>Security and privacy Information flow control</concept_desc> <concept_significance>500</concept_significance> </concept> <concept> <concept_id>10011007.10011006.10011041</concept_id> <concept_desc>Software and its engineering Compilers</concept_desc> <concept_significance>300</concept_significance> </concept> </ccs2012>
\ccsdesc[500]Security and privacy Logic and verification \ccsdesc[500]Security and privacy Information flow control \ccsdesc[300]Software and its engineering Compilers \relatedversion\supplementThe Isabelle/HOL theories are available at https://covern.org/itp19.html.
Acknowledgements.
We would like to thank our anonymous reviewers, as well as Carroll Morgan, Kai Engelhardt, Gerwin Klein, Christine Rizkallah, Matthew Brecknell, Johannes Åman Pohjola, and Qian Ge, for their very helpful feedback on earlier versions of this paper.\EventEditorsJohn Harrison, John O’Leary, and Andrew Tolmach \EventNoEds3 \EventLongTitle10th International Conference on Interactive Theorem Proving (ITP 2019) \EventShortTitleITP 2019 \EventAcronymITP \EventYear2019 \EventDateSeptember 9–12, 2019 \EventLocationPortland, OR, USA \EventLogo \SeriesVolume141 \ArticleNo5
Verifying that a compiler preserves concurrent value-dependent information-flow security
Robert Sison
Toby Murray
Abstract
It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties—in which classification of locations can vary depending on values in other locations—and complicated further when programs exploit shared-variable concurrency.
Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition principles for separating it into smaller, more familiar, proof obligations.
In this work, we provide such a decomposition principle, which we show can almost halve the complexity of proving secure refinement. Further, we demonstrate its applicability to secure compilation, by proving in Isabelle/HOL the preservation of value-dependent security by a proof-of-concept compiler from an imperative While language to a generic RISC-style assembly language, for programs with shared-memory concurrency mediated by locking primitives. Finally, we execute our compiler in Isabelle on a While language model of the Cross Domain Desktop Compositor, demonstrating to our knowledge the first use of a compiler verification result to carry an information-flow security property down to the assembly-level model of a non-trivial concurrent program.
keywords:
Secure compilation, Information flow security, Concurrency, Verification
category:
\hideLIPIcs
1 Introduction
It is well known that program translations of the kind carried out by compilers can in principle break security properties like confidentiality [12, 2]. Yet source level reasoning about confidentiality remains common [20, 19, 18]. Existing verified compilers like CompCert [15] and CakeML [14] preserve semantics, but semantics preservation alone may be insufficient to preserve confidentiality, especially for shared memory concurrent programs whose threads must guard against timing leaks in order to prevent them manifesting as storage leaks [22].
Supporting secure compilation of programs that must enforce value-dependent security policies poses an additional challenge, because in such policies the sensitivity of a memory location can depend on the values held in other memory locations. Thus, unlike prior work on secure compilation [4], preserving security under refinement requires a refinement relation that is strong enough to preserve those memory contents on which the policy depends.
In prior work [22], we presented a definition for a notion of value-dependent security-preserving refinement that is compositional for concurrent programs: by applying it to each thread individually, one can derive a secure refinement of the concurrent composition.
The essence of this notion of security-preserving refinement (presented fully in Section 2.2) is in its refinement preservation obligation ( in Figure 1). Here, the usual square-shaped commuting diagram that is commonly used to depict (semantics-preserving) refinement (Figure 4(a)) has been replaced by a cube (Figure 1). The additional dimension of this cube reflects that it preserves a 2-safety hyperproperty [6] that compares two executions rather than examining a single one. As such, it is significantly more complicated to prove than standard notions of semantics-preserving refinement typical in verified compilation [15, 14].
To date there exist no verified compilers for shared-variable concurrent programs proved to preserve value-dependent information-flow security. We argue that without a decomposition principle the cube-shaped refinement notion is too cumbersome to prove for realistic compilers.
In this paper, we tackle the central problem of making our notion of secure refinement applicable to verified secure compilation. Firstly, we present a decomposition principle that makes the cube-shaped notion more tractable. Secondly, we demonstrate its tractability with our major contribution: a machine-checked formal proof of concurrent value-dependent security preservation, for a proof-of-concept compiler.
In Section 3 we present our decomposition principle, which decomposes the cube (Figure 1) into three separate obligations (Figure 4). The first of these is akin to semantics-preserving refinement, while the second and third essentially ensure together that the refinement has not introduced any termination- and timing-leaks.
In Section 4 we show how the decomposition principle can almost halve the effort to prove secure refinement – in this case, of a program that is especially prone to introduced timing leaks because it branches on secrets (a feature not yet allowed by our compiler). There, we present a side-by-side comparison of the proof effort, both with and without the decomposition principle. We find that using it reduces the proof’s complexity by 44%.
In Section 5, we present our compiler and its formal verification, as an application of the decomposition principle. This compiler translates concurrent programs written in an imperative While language, with locking primitives for mediating access to shared memory, into a RISC-style assembly language. It does so by compiling each thread individually, and in doing so preserves a formal security property that remains compositional between threads. Furthermore, our compiler demonstrates a way of formalising and proving when it is safe for a compiler to perform optimisations in the presence of concurrency. To ensure that the contents of shared memory locations are preserved under compilation despite potential interference from other threads, our compiler tracks which shared memory locations are stable (free from any such interference). It then makes use of this tracking to avoid redundant loads from stable shared variables safely, that would otherwise be considered unsafe to omit.
All results are mechanised in Isabelle/HOL,111The wr-compiler totals 7k lines, and verification + compilation of the 2-thread CDDC model totals 1.6k lines of Isabelle proof script, excluding whitespace and comments. See “Supplement Material”. and in Section 6 we explain how, in order to validate our theory, we instantiated it so that we could execute our compiler in Isabelle. This enabled us to execute it over a While language model of the Cross Domain Desktop Compositor [5] (CDDC), a concurrent program that enforces information flow control over value-dependently classified input. To our knowledge this is the first proof of information flow security for an assembly-level model of a non-trivial concurrent program, demonstrating the power of verified secure compilation for deriving security properties of compiled code.
2 Background and example
We begin by introducing with an illustrative example (Figure 2) the challenges of verifying value-dependent information-flow security in the presence of shared-variable concurrency.
Consider the task of verifying a multithreaded system that manages the user interface (UI) for a dual-personality smartphone, a phone that provides clearly distinguished user contexts (personalities), typically for work versus leisure. Specifically, our task is to verify that it does not leak sensitive information intended only for one of those personalities, which we classify (2(c)), to locations belonging to the other, which we classify (2(c)).
Here and generally, our attacker model is an entity that can read from the system’s untrusted sinks: some subset of permanently -classified locations not subject to synchronisation. In our example, this may include WLAN device registers in a hostile environment.
The smartphone’s UI system consists of a number of threads running concurrently with a shared address space, and we aim to verify that as a whole it satisfies the security requirement. But to avoid a state space explosion that is exponential in the number of threads, we must do this compositionally: one thread at a time, then combining the results of these analyses.
We focus on a particular worker thread (2(a)), the one responsible for sending touchscreen input from the variable to its intended destination.
The first challenge is that the destination depends on which personality the phone is currently providing, which is indicated by the value of . This is reflected by the classification of being dependent on the value of : is classified exactly when (where LOW is a designated constant), and is classified otherwise. Due to this dependency, is known as a control variable of .
The second challenge is the worker thread runs in a shared address space that might be accessed or modified by other threads, for various purposes. One of these threads may be responsible for maintaining that exactly when the phone indicates it is providing the personality (2(c)), so the user knows not to type in anything sensitive. Another thread may be responsible for assigning when the user turns the phone’s screen off, to make the worker stop processing touchscreen input. We may then wish for to be usable by some other thread—e.g. processing input from a fingerprint scanner—in such a way that it can assume no longer contains any sensitive values.
When we analyse one thread like this worker in terms of our compositional security property (Section 2.1), all of the other threads in the system are trusted to do two things:
They follow a synchronisation scheme: here, if read- or write-access to a certain variable is governed by a lock, they must hold it in order to access the variable in that manner. 2. 2.
They themselves do not leak values from -classified locations (we refer to such values themselves as ) to -classified locations that are read-accessible to other threads. Note we are proving that the thread we are analysing can be trusted in the same way.
Even under these assumptions, the concurrency gives rise to some tricky considerations.
Firstly, it is important that no thread in the system (including the thread under analysis) modifies any control variables carelessly. For example, writing immediately after the worker reads a value from , will cause it to leak to . To prevent this, the worker uses , granting it exclusive write-access to and .
Furthermore as noted above, we may want to ensure that a non-attacker-observable location is nevertheless cleared of any sensitive values before being used by another thread. In our example, we classify for the analysis to enforce this when the worker is suspended, but as the worker sometimes uses it to process values, it is important to know is accessible only to the worker during that time. To ensure this, the worker uses , granting it exclusive read- and write-access to . It is then responsible for clearing it of any values by the time it releases exclusive read-access.
2.1 Concurrent value-dependent noninterference (CVDNI)
Having illustrated the challenges with an example, we now focus on the formalisation of our information-flow security property CVDNI, which we target with our per-thread analysis, and which our compiler preserves. It is defined in terms of two main elements:
a binary strong low-bisimulation (modulo modes) relation between program configurations, that establishes the required information-flow security property. Like Goguen & Meseguer-style noninterference [10], any states it relates must agree on their “low” portions, and it demands that lock-step execution preserve that correspondence. This section will explain how it is specialised further for shared-variable concurrency. 2. 2.
a classification function that determines the “low” portion of a program configuration, thus affecting ’s requirements. Unlike [10] however, here can depend on values in the program configuration itself, thus expressing dynamic and not just static classifications.
We now present definitions from Section III-2b of our previous work [22] simplified as noted. The theory is parameterised over the type of values , a finite set of shared variables , and a deterministic evaluation step semantics between local configurations (of a thread in a concurrent program) each denoted by a triple :
- •
is the thread-private state, which is permanently inaccessible to the attacker and the other threads. Note that due to this inaccessibility, we allow the user of the theory to parameterise the type of , and do not impose any particular structure.
- •
is the (access) mode state, which is ghost state associating each with a set of shared variables. Intuitively, it identifies the set of variables for which the thread currently possesses (or respects) a kind of exclusivity of access granted (or obligated) by a synchronisation scheme. This facilitates compositional, assume-guarantee [11] style reasoning. For example, when our worker thread holds , it assumes no other threads write to or its control variable (), otherwise it guarantees it does not write to them (). Similarly, holding it assumes no other threads read or write to (), and at all other times it makes the corresponding guarantee ().
- •
is shared memory considered potentially accessible to the attacker and other threads. In order to make what is accessible amenable to analysis, we impose the structure , a total map from shared variable names to their values.
The theory is then further parameterised by the value-dependent classification function , and a function that returns all the control variables of a given variable. In our worker thread example, gives:
- •
when is , meaning is classified at all times.
- •
when is : if , and otherwise.
- •
for all other variables , meaning they are classified at all times.
The set is then defined to contain all control variables in the system. Thus in our worker thread example, and .
To support compositionality for concurrent programs, the “low” portion demanded to be equal by the analysis is tightened up to be modulo modes – it includes non-control variables only if they are assumed to be readable by other threads according to the mode state: . Thus intuitively, the user of the theory should model permanent untrusted output sinks of the whole concurrent program, as variables for which always returns , ungoverned by any synchronisation scheme that the attacker cannot be trusted to follow. (In our example, is untrusted permanently in this way, but is untrusted only when unlocked.) The notion of observational indistinguishability used for the noninterference property is then defined over memories as follows.
Definition 2.1** (Low-equivalent memories modulo modes).**
[TABLE]
For this paper, we will use notation to lift to local program configurations, asserting also that and are modes-equal (have the same mode state). Additionally, we will use notation to denote (alone) that and are modes-equal.
The per-thread compositional security property asserts the existence of a witness relation for every possible observationally equivalent pair of starting configurations:
Definition 2.2** (Per-thread compositional CVDNI property).**
[TABLE]
where all such witness relations must be a strong low-bisimulation (modulo modes):
[TABLE]
That is, must maintain observational indistinguishability by requiring that all configuration pairs it relates that have the same mode state, are low-equivalent modulo modes.
Furthermore, it must be a bisimulation by being symmetric and progressing to itself: any step taken by one of the configurations must be able to be matched by a step taken by the configuration related to it, such that the destinations remain related by (and modes-equal).
Finally—and the most crucial element ensuring the property’s compositionality for concurrent programs—is the condition that must be : closed under globally consistent changes made to memory by other threads, which is to say, changes that preserve low-equivalence and are permitted by the current mode state . Specifically, the environment (of other threads) is permitted to change either of variable ’s value or its classification only when is writable: .
Definition 2.3** (Closedness under globally consistent changes).**
[TABLE]
Theorem 3.1 of our prior work [22] then gives us that the parallel composition of programs is itself a program that enforces a system-wide value-dependent noninterference property (, for whose details we refer the reader to Section III-2(a) of [22]).
2.2 CVDNI-preserving refinement
Having described the formal security property that we wish to be preserved under refinement (and compilation), we now define formally a suitable notion of secure refinement that preserves it. The proof of CVDNI-preserving refinement for a thread of a concurrent program relies on two binary relations (illustrated by Figure 3) to be nominated by the user of the theory:
a refinement relation relating local configurations of the abstract program to local configurations of the concrete program: abstract must simulate concrete, in a sense typical of much other work on program refinement, including compiler verification efforts. 2. 2.
a concrete coupling invariant that allows us to use and to build a new strong low-bisimulation (modulo modes) for the concrete program, by discarding unreachable pairs of local configurations after the refinement. It thereby witnesses that any changes a refinement (or compiler) makes to execution time, do not introduce any timing channels.
The essence of the proof technique is to require that a number of conditions—analogous to those for —be imposed on the nominated and in relation to a given witness relation establishing CVDNI for the abstract program. The definitions to follow are adapted from Murray et al. [22] Section V. For better readability, we present a simplified version in which no new shared variables are added by the refinement. Consequently we introduce the notation to denote that two local configurations have equal mode state and memory, regardless of whether relating configurations of the same or differing languages.
Regarding the maintenance of modes- and observational-equivalence across the relation, the restrictions on refinement are tighter than those that applied to . The refinement relation is required to preserve the shared memory in its entirety:
Definition 2.4** (Preservation of modes and memory).**
[TABLE]
Regarding the closedness under changes by other threads that ensures compositionality for concurrency, on we again impose (2.3) from Section 2.1. However in the case of , we instead impose , a simplification of considering only environmental actions that affect the memories on both sides of the relation identically. Furthermore it ensures equality of all shared variables, not just those judged observable:
Definition 2.5** (Closedness of refinements under changes by others).**
[TABLE]
The final major requirement for CVDNI-preservation is then to prove and closed simultaneously under the pairwise executions of the concrete and abstract programs, using the aforementioned cube-shaped diagram (, Figure 1) whose edges are pairs in , , and . All that then remains is for the nominated concrete coupling invariant to be symmetric, and the predicate puts together all the requirements:
Definition 2.6** (Requirements for secure refinement of the per-thread CVDNI property).**
[TABLE]
Theorem 5.1 of our prior work [22] gives us that under the aforementioned conditions,
[TABLE]
is a witness for the concrete program:
[TABLE]
3 Decomposition principle for CVDNI-preserving refinement
Having presented our previous work [22]’s formalisation of our security property CVDNI and its preservation by refinement, we now present our first contribution: an alternative way of proving (2.6) that does away with the use of the cube-shaped, two-sided refinement obligation (depicted by Figure 1), by decomposing its concerns into (1) proving closed under the pairwise executions of the concrete and abstract programs alone using a square-shaped diagram (depicted by 4(a), which is akin to ordinary semantics-preserving refinement), and (2) a number of smaller and more separable obligations gathered together under the side-condition predicate .
Definition 3.1** (Decomposed requirements for CVDNI-preserving secure refinement).**
[TABLE]
The decomposition requires the provision of a new refinement parameter that we will call or the pacing function, whose role is to dictate the pace of the refinement by returning the number of abstract steps that ought to be taken for a single concrete step, for a given abstract-concrete local configuration pair related by . The side-conditions on all of the refinement parameters (depicted by Figures 4(b), 4(c)) are then defined as follows:
Definition 3.2** (Side-conditions for CVDNI-preserving refinement decomposition).**
[TABLE]
On the intuitive meaning of the side-conditions in 3.2:
- •
ensures that the refinement has not introduced any termination leaks, by asserting consistent stopping behaviour for -related concrete program configurations, which we know to be observationally indistinguishable.
- •
ensures that the refinement has not introduced any timing leaks, by asserting consistency of the pace of the refinement for -related program configurations, which we again know to be observationally indistinguishable.
- •
The final -quantified clause asserts ’s suitability as a coupling invariant, in that it must remain closed under lockstep evaluation of the concrete program configurations it relates. Furthermore it must maintain mode state equality with each lockstep evaluation, which ensures that the refinement has not introduced any inconsistencies in the memory access assumptions and guarantees needed for the concurrent compositionality of the property.
Note the - and -edges in 4(c) may capture useful facts about a particular program verification technique and compiler, so their availability as assumptions is intended to reduce greatly the effort needed to specify a coupling invariant and prove it satisfies the condition.
Assuming the fulfilment of all of the decomposed requirements, we obtain that they are a sound method for establishing secure refinement of the per-thread CVDNI property:
Theorem 3.3** (Soundness of ).**
[TABLE]
In the interests of brevity we relegate proof sketches for all results to Appendices C and D, and for fuller details we refer the reader to our Isabelle/HOL formalisation.
We now devote our attention to two instantiations of this new decomposition principle: (Section 4) for a proof of CVDNI-preservation for the refinement of a program that branches on a secret, and (Section 5.5) for the proof of CVDNI-preservation by a compiler.
4 Proof effort comparison
To demonstrate how the decomposition principle reduces proof complexity and effort, we returned to the example refinement discussed in Section V-E of our previous work [22], an excerpt of which is shown in Figure 3. The abstract program (9 imperative commands) branches on a sensitive value, and executes a single atomic expression assignment in each branch. Its refinement (to 16 commands) models expansion of the expressions into multiple steps, resolving a timing disparity between the two branches by padding with skip.
We use proof size as a proxy for proof effort, since the former is known to be strongly linearly correlated with the latter [28]. Formalised in Isabelle/HOL as EgHighBranchRevC.thy [21], the proof line count for that theory stood at about 4.6K lines of definitions and proof, of which approx. 3.6K line were proofs. Adapting the proof instead to use the decomposition principle (3.1), the proof line count drops from 3.6K to approx. 2K, a 44% reduction. Regarding definition changes, the new proof makes <10 lines of adaptations to a coupling invariant and pacing function used by the old proof, and adds about 30 lines worth of new helper definitions, for use with the decomposition principle. The rest of the theory and its external dependencies remain in common between the two versions.
As would be expected, the bulk of the deletions are from the full cube-shaped refinement diagram proof (Figure 1) of (2.6) for the refinement relation. The surviving parts of that proof just become the square-shaped refinement diagram proof (4(a)) of without much modification. The deletions are replaced by newly added proofs of the three sub-obligations of (3.2).
5 The Covern wr-compiler
Having presented our new decomposition principle for CVDNI-preserving refinement, we now turn to our compiler, whose most notable features for formal proof of secure refinement are:
Its implementation tracks variable stability (Section 5.4) responsive to use of locking primitives, to know when accesses to shared variables are safe to optimise, and when register contents can be still be considered consistent with shared variable contents. 2. 2.
Its verification uses a pacing function (Section 5.5.2) and coupling invariant (Section 5.5.3) as the decomposition demands, to ensure it does not introduce timing leaks.
First, we describe its source and target languages, and parameters to the compilation.
5.1 Source language
The Covern wr-compiler—short for While-to-RISC compiler—takes the simple imperative language with while-looping and lock-based synchronisation targeted by the Covern program logic [20], which we will refer to as While, consisting of the commands :
[TABLE]
The language is parameterised over a type of values , and binary operators . Constants ; and are (resp.) shared program- and lock-variables. The semantics of the locking primitives and is informed by a locking discipline provided by the user of the theory as a parameter (see Section 5.3). We leave for future work adding support for pointers and arrays, which we believe will be straightforward because our assume-guarantee framework already provides the means to encode the memory footprint of a command in a way that depends on values in memory.
We assume that the underlying concurrent execution model (e.g. operating system, scheduler) for the While language prevents threads from seeing each others’ current program location, and thus (as in previous work [22, 19]) the While program command being executed we model as thread-private state: . In contrast, all program variables and lock variables reside in the shared memory .
5.2 Target language
The wr-compiler’s target is a generic RISC-style assembly language like that of Tedesco et al. [29] but with lock-based synchronisation primitives added, which we will refer to as RISC:
[TABLE]
The language is parameterised over the same value type and binary operators , shared program variables and shared lock variables as the While language. Presently, direct-addressing Load and Store instructions (referring to registers ) are adequate for RISC to implement all existing While features, and we expect adding indirect addressing to RISC to be as straightforward as adding pointer and array support to While.
RISC program texts are just lists of binary instructions , each optionally associated with a label . We assume that the underlying concurrency model for the RISC language (e.g. OS, scheduler etc.) prevents one thread from reading the program code (instructions) of another,222As is usual for program analyses, we omit any explicit modelling of the microarchitectural state used by superscalar processors (like CPU caches, and state relied on by speculative and out-of-order execution, on whose behaviour attacks like Spectre [13] and Meltdown [16] relied). We argue however that our present assumptions are reasonable under two circumstances: when there is no such state (e.g. on microcontrollers like AVR [7]), or when such state is correctly partitioned by the underlying hardware [30] or the OS [8] – if the hardware allows it [9]! In the latter case, our analysis assumes that microarchitectural state footprints are partitioned according to thread (for memory containing program text) and according to classification by (for shared memory), and furthermore that each value-dependently classified region is given a distinct partition that is flushed on reclassification. as well as another’s registers (including the program counter). Thus, we model the distinguished program counter register’s value , program text , and register bank as thread-private state: . Apart from this adaptation to our triple format, evaluation semantics follows that of the RISC target of [29].
Finally, like Tedesco et al. [29] we generalise over the (user-supplied) register allocation scheme, and assume there are enough registers to service the maximum depth of expressions in the source program. (More details are available in Appendix D.1.) We leave for future work the modelling and analysis of a compiler phase that spills register contents to memory, in order to make this assumption unnecessary.
5.3 Locking discipline
Like the Covern logic [20], we assume that the While language program being compiled follows a certain locking discipline, about which the compiler has knowledge, so as to ensure that the RISC program it produces follows the same discipline.
The user of the theory provides the details of the locking discipline in the form of a lock interpretation parameter: , which for each lock gives the two non-overlapping sets of program variables over which acquiring the lock grants exclusive permission to write, (resp.) read and write. These permissions are then reflected in the way the semantics of the While and RISC locking primitives act on the mode state.
Regarding lock interpretations and the way they interact with the user-provided value-dependent classification function (see Section 2.1), we inherit a few cleanliness conditions from that earlier work [20], chief of which are that lock variables cannot be control variables, a lock variable governing access to a program variable must govern the same kind of access to all of ’s control variables, and must classify all lock variables as .
5.4 Compiler implementation and tracking of shared variable stability
We chose as a starting point the compilation scheme of [29], on the basis of their preserving a noninterference property that like ours exhibits resilience to changes made by an environment—in their case, intended for fault-resilience. Aiming to repurpose that for shared-variable concurrency, we adapted it to Isabelle, implementing it as a primitive recursive function:
[TABLE]
where we choose for RISC instruction labels, and the compilation record type is bookkeeping maintained by the compiler that we will describe further below.
A typical invocation to compile a While program takes the form:
[TABLE]
Here, takes an initial compilation record , an optional entry label , and the next available label , and for the benefit of the next invocation returns an optional exit label if one is used by the program just compiled, the new next available label , and a final compilation record . We leave details of label allocation and its impact on achieving sequential composability for compiled RISC programs to Appendix D.2.
In addition to the output RISC program itself, a call to also outputs every associated with the state of the program just before executing every instruction in . These are returned zipped up together with as the -annotated RISC program . ( can trivially be recovered as .) Finally, may return for to reject the input program, such as when it detects a data race (see below), or if expression depth exceeds the assumed limit (Section 5.2).
In the style of the compilation scheme on which it was based [29], the wr-compiler maintains a register record , i.e. a partial map of registers to expressions on shared variables. In addition to using it to compile away any unnecessary loads from variables in shared memory, we also use it to ensure that an expression calculated by RISC in registers is equal to the value of the expression as if it had all been calculated by While in one step. This is especially important when writing the result of an expression back to shared memory, because the refinement is required to maintain all shared memory values.
New to the wr-compiler is the responsibility of maintaining an assumption record, which it uses primarily to detect and reject programs with data races on shared memory, and to rule out the introduction of any new ones. Each assumption record is a pair tracking the set of variables on which (resp.) AsmNoW, AsmNoRW assumptions are currently active at a given point in the program being compiled. As a secondary concern we also use it to assert that the two sides of any if-conditional branches act consistently on the mode state, and that while-loops restore the original mode state on termination.
A compilation record is then just a register/assumption record pair. For readability, we use , to denote (resp.) a ’s , projections.
To explain how the compilation record is used to rule out data races, and to ensure consistency of expression evaluation between source and target program, firstly we must introduce the concept of stability of a variable according to an assumption record :
[TABLE]
In short, this means that the variable and all its control variables () are recorded as having either of AsmNoW or AsmNoRW active on them.
For register record entries to be of any help in ensuring consistency of While and RISC expression evaluation, we exclude expression evaluation on data race-prone variables by lifting the concept of stability to register records. The following predicate asserts internal consistency of the compilation record created by , in the sense that the register record may only map to expressions that mention variables that are recorded as stable by the assumption record accompanying it. (Here, denotes the range of a map.)
[TABLE]
To ensure that an input While program maintains register record stability, we define the predicate no-unstable-exprs to capture the requirement that a program , if started with a configuration consistent with compilation record , will never access a lock-protected variable without holding the relevant lock. (It also checks the secondary, mode-state consistency concerns of the assumption record mentioned earlier.) We implement it as a simple static check carried out by a primitive recursive function on the structure of While programs.
Together, and no-unstable-exprs make up the main two requirements of a predicate imposed on the input arguments to , which gives us enough information to prove a lemma that only ever outputs stable register records. Full details of these we leave to Appendix D.3.
5.5 Proof of CVDNI-preserving compilation
Having covered the most significant aspects of the Covern wr-compiler’s parameters and machinery, we can now present the refinement relation (Section 5.5.1), pacing function (Section 5.5.2), and coupling invariant (Section 5.5.3) that we use with our new decomposition principle (of Section 3) to prove that it preserves CVDNI (Section 5.5.4).
5.5.1 Refinement relation and its invariants
Just like our example of Figure 3, pairs abstract with concrete configurations.
Here, we will focus on ’s most notable characteristics for understanding why it is suitable to describe a CVDNI-preserving compilation.333We provide an informal description of all of the cases, their purpose, and the invariants they maintain, along with a code listing from relevant to the part that will be presented, in Appendices A and B (respectively). For full details, we refer the reader to the Isabelle formalisation. We focus on the case of , which relates the expression evaluation part of the While program , with the corresponding part (including the conditional jump Jz after expression evaluation) of the RISC program obtained by running on it. (Variables ignored are in gray.)
Example 5.1** (Introduction rule for case if_expr of ).**
[TABLE]
This is a fairly typical case of in a number of respects:
Firstly, there is a direct reference to the call to for the given While program. Secondly, various guards ( introduced below, and defined in Section 5.4) are asserted in order to restrict the scope of only to consider wellformed local program configurations that line up with the conditions captured by the compilation record. Thirdly, the inductive references to for and , the branches of the conditional that have not been reached yet, are quantified over all configurations that obey the guards and relative to , the initial compilation record for each of the sub-calls to for those sub-programs.
The guard mentioned above asserts that the compilation record is consistent with the registers , memory and mode state .
[TABLE]
Firstly, for all entries in register record mapping some register to some expression , the value held in of the register bank must match the value of if evaluated under memory . Secondly, the assumption record must consist exactly of the program variables the mode state says have AsmNoW, AsmNoRW on them respectively.
As we will see in Theorem 5.8, also serves as initial configuration requirements for compiled programs: only configurations obeying them may be used to initialise a RISC program compiled by the wr-compiler with initial compilation record .
With specified, we then prove the two requirements for that pertain to alone: (2.4) and (2.5).
Lemma 5.2** ( preserves modes and memory).**
**
Lemma 5.3** ( is closed under changes by others).**
**
5.5.2 Refinement pacing function
We now nominate an function, determining the pace at which While programs progress in comparison to the RISC programs that they are compiled to by the wr-compiler.
To assist here and elsewhere, we define a primitive recursive helper leftmost-cmd that given a sequence of ;-separated While commands, strips all but the first: given it returns leftmost-cmd , and given any other While program it returns .
Our pacing function primarily looks at the form of the RISC program instruction about to be executed. The RISC instructions are divided into three categories:
- •
Instructions output by : Load, Op, and MoveK. For these, returns 1 if the leftmost-cmd of the While program is , to allow it to step to concurrently with the first RISC step of the compiled expression itself. Otherwise, returns 0 to indicate the While program standing still while the RISC program takes new steps to evaluate the expression.
- •
“Epilogue” steps: Jmp and Nop when used for control flow at the end of a smaller compiled program in the context of a larger one. For these, returns 0.
- •
All other RISC instructions are assumed to proceed at a lockstep pace with the While command they were compiled from, and for these returns 1.
Having nominated and , we now have the parameters over which we are obliged to prove refinement preservation (4(a)) as demanded by (3.1). To this end, we prove firstly (elided to Appendix D.3) that every step of execution of a RISC program produced by the wr-compiler from a While program, maintains the consistency demanded by between configurations and compilation records. Also, we must prove a correctness lemma for the expression compiler:
Lemma 5.4**.**
**
Armed with these facts, we can now prove the main refinement preservation result:
Lemma 5.5** ( is a refinement paced by ).**
[TABLE]
5.5.3 Concrete coupling invariant
The next element needed is the concrete coupling invariant , which we define as follows:
In other words, asserts that we only need compare local configurations that are at the same location of the same RISC program . When used in concert with a (see Section 5.5.4), the effect of is to ensure that the wr-compiler has not introduced any new branching on sensitive values.
5.5.4 Successful compilations are CVDNI-preserving refinements
We are ready to prove preservation. First we qualify that we allow only that describe only While-programs with no branching on -classified values, as follows:
[TABLE]
That is, it refuses to relate configurations at different program locations. Furthermore if it is at a conditional branching point, the expression determining which branch will be taken evaluates to the same boolean value for both configurations’ memories. When imposed on a relation that already ensures -equivalent memory modulo modes, this effectively disallows any present or past branching on sensitive values. Then, for such programs:
Lemma 5.6**.**
**
From this it follows immediately via Theorem 3.3 that with the help of describes a CVDNI-preserving refinement for non--branching While programs:
Corollary 5.7** ( is a CVDNI-preserving refinement for non-High-branching programs).**
[TABLE]
Finally, we prove that successful compilation produces a RISC program related by to its input While program, when started with corresponding and reasonable initial configurations:
Theorem 5.8** (Successful compilations are refinements in ).**
[TABLE]
6 Case study: the wr-compiler in action
To test the theory, we instantiated it and applied the wr-compiler to a While-language model of the Cross Domain Desktop Compositor [5] (CDDC), a non-trivial concurrent program that facilitates a trusted user’s interaction with multiple desktop machines of differing clearance.
The CDDC model to which we applied the compiler is a 2-thread program that was a precursor to the 3-thread model that was verified using the Covern program logic [20].444We leave for future work an adaptation of the refinement theory and wr-compiler in order to support the shared data invariants added by the Covern logic, required to verify the 3-thread CDDC model. Each of the threads of the CDDC program (together about 150 lines of While) we proved satisfy the compositional security property (2.2), using a precursor to the Covern logic that yields CVDNI-witness bisimulations that are non--branching.
The resulting compiler is executable in Isabelle, meaning that can be executed on the While program text for each of the two threads to obtain their compilations (together totalling about 250 RISC instructions) using the Isabelle tactic eval. The secure compilation theorems (Section 5.5.4), together with preservation and compositionality for (Theorems 5.1, 3.1 of [22], mentioned in Section 2) then allow us to derive that the compiled program is secure when its threads are run concurrently.
To our knowledge this is the first proof of source-level information-flow security being carried by a verified compiler to an assembly-level model of a non-trivial concurrent program.
7 Related work
The following three works, like ours, focus on compilation preserving a form of noninterference.
Tedesco et al. [29] present a type-directed compilation scheme that preserves a fault-resilient noninterference property. The compilation scheme of our wr-compiler was inspired by theirs. Like our CVDNI security property that wr-compiler preserves, Tedesco et al.’s security property is also strong bisimulation-based [27]. But where our property accounts (via mode states) for controlled interference by other threads, theirs instead quantifies over all possible interference by the environment with the memory contents. While this simplifies their task of proving that their security property is preserved under compilation—as it need not require the compiler to preserve the contents of memory—it means their security property cannot capture value-dependent noninterference. In contrast, our wr-compiler must obey our notion’s requirement that memory contents are preserved.555Consequently, we found and fixed a bug in their expression compiler (acknowledged privately) whereby registers in use were incorrectly reallocated. Expressions like were thus compiled incorrectly to programs yielding instead, causing a violation of memory contents preservation.
Barthe et al. [2] consider the problem of preserving cryptographic constant-time policies, a class of noninterference properties similar to CVDNI in its explicit consideration for capturing timing-sensitivity. Barthe et al. consider a wider scope of common categories of compile-time optimisations (than those performed by our wr-compiler), and mechanise proofs in Coq that such optimisations preserve various constant-time security properties. The sharing of variables in our setting severely limits the scope of our optimisations, to those that the compiler can perform knowing that a shared variable is stable because it has been locked. At present, our wr-compiler avoids redundant loads during expression compilation, but other optimisations like loop hoisting and constant folding we are yet to implement. Their preservation proof technique, constant-time simulation was developed independently to our original cube-shaped secure refinement definition [22]. Like ours, theirs is also a cube-shaped obligation and makes use of a pacing function analogous to our . Unlike our work here, Barthe et al. do not give a general method for decomposing their cube-shaped simulation diagrams.
Neither of the above consider per-thread compositional compilation of concurrent, shared memory programs, nor value-dependent noninterference policies – the focus of our theory and compiler. Barthe et al. [4] however did aim to preserve noninterference of multithreaded programs by compilation, extending a prior (security) type-preserving compilation approach [3]. Their noninterference property however was termination- and timing-insensitive, so preventing internal timing leaks relied on the scheduler disallowing certain interleavings between threads. Also, their type-preservation argument was derived from a big-step semantics preservation property for their compiler. Here we instead rely on preservation of a small-step semantics (specifically memory contents), which is necessary for us to preserve value-dependent security under compilation, as well as to avoid imposing non-standard requirements on the scheduler.
Other recent works have improved on fully abstract compilation (surveyed [23]) by mapping out the spectrum [1] or developing specific forms [25] of robust property preservation, concerned with robustness of source program (hyper)properties to concrete adversarial contexts. Like Tedesco et al. [29], these works differ from ours in quantifying over a wider range of hostile interference. They also focus prominently on changes to data types, which we do not support. Thus, as a 2-safety hyperproperty quantifying over a lesser range of interference, we expect CVDNI-preservation to be implied by R2HSP (robust 2-hypersafety preservation), but do not expect it to imply any other secure compilation criterion on Abate et al.’s [1] spectrum.
While recently Patrignani and Garg [25] instantiated their robustly safe compilation for shared-memory fork-join concurrent programs, it only preserves (1-)safety properties. Previously however, Patrignani et al. [24] proved their trace-preserving compilation preserves -safety hyperproperties [6], including noninterference properties. However, it disallows the removal or addition of trace entries, which would be necessary to change the passage of time as seen in the observable trace events. Thus it excludes optimisations carried out by our compiler (when it permits changes to pacing regulated by ) and studied by the two other works [29, 2] on timing-sensitive security-preserving compilation mentioned above.
Finally, there has been much work on large-scale verified compilation [15, 14] some of which has also treated compilation of shared-memory concurrent programs [17] including taking weak-memory consistency into account [26]. Our work here does not consider the effects of weak-memory models. However, it differs to prior work on verified concurrent compilation, in that it formalises and proves a compiler’s ability to use information about the application’s locking protocol, to exclude unsafe access to shared variables, and conversely to know when it is safe to allow optimisations that would typically be excluded (see Section 5.4).
8 Conclusion
To our knowledge, we have presented the first mechanised verification that a compiler preserves concurrent, value-dependent noninterference. To this end, we provided a general decomposition principle for compositional, secure refinement. Although our compiler is a proof-of-concept targeting simple source and target languages, we nevertheless applied it to produce a verified assembly-level model of the CDDC [5], a non-trivial concurrent program.
This work serves to demonstrate that verified security-preserving compilation for concurrent programs is now within reach, by augmenting traditional proof obligations for verified compilation (e.g. square-shaped semantics preservation) with those specific to security (e.g. absence of termination- and timing-leaks) as depicted in Figure 4. We hope that this work paves the way for future large-scale verified security-preserving compilation efforts.
Appendix A Informal descriptions of the cases of refinement relation
A.1 Base cases
- •
stop: This case relates a terminated While program with a terminated RISC program (i.e. one where the program counter is at the length of the program text).
- •
skip_nop: This case relates the While program skip with the configuration where the program counter is at the start of the RISC program .
- •
assign_expr: This case relates the expression evaluation part (for the expression ) of the While program with the corresponding part of the RISC program obtained by compiling it with the wr-compiler.
- •
assign_store: As for assign_expr, but for the very last Store instruction that commits the result of the expression evaluation back to shared memory variable .
It asserts additionally that must be stable if lock-governed, and non-lock-governed otherwise. This prevents threads from violating the locking discipline (see Section 5.3).
- •
lock_acq: This case relates with .
- •
lock_rel: This case relates with .
A.2 Inductive cases
- •
seq: This case relates the While program with the concatenation of the RISC programs and that are respectively the outputs of successful consecutive compilation of and by the wr-compiler. It is intended for cases where the While (resp. RISC) program is currently in (resp. ).
It is an inductive case of , in that:
- –
is required to be related by to the present location in .
- –
For all local configurations that obey the requirements, is required to be related by to the first instruction of . This quantification ensures that remains closed when execution progresses from the first program to the second program.
It asserts that and are (Section D.2), particularly relevant here to ensure that can only jump to locations within or at the end of itself (i.e. the start of ).
- •
join: This case relates a While program with an offset into a RISC program , assuming the inductive hypothesis that is related by with the offset into the RISC program alone.
It is intended primarily for cases where the While (resp. RISC) program is currently in the (resp. ) of some consecutively compiled (resp. concatenated with ) but applies more broadly to allow any prepend of dead, unreachable instructions onto the front of a RISC program without breaking .
It also asserts that and are , which is important here to ensure that cannot jump back into .
- •
if_expr: This case relates the expression evaluation part (for the expression ) of the While program with the corresponding part (including the conditional jump Jz at the end of expression evaluation) of the RISC program obtained by compiling it with the wr-compiler.
It relies on both and being related by to its compiled RISC counterparts when started with initialisation states judged valid by .
- •
if_c1: This case relates some While program reachable from with the corresponding part within the part of the RISC program obtained by compiling with the wr-compiler.
It relies on being related by to its compiled RISC counterpart at the appropriate program counter offset.
- •
if_c2: As for if_c1, but for .
- •
epilogue_step: This case relates a terminated While program to the silent control flow steps navigating to the end of a RISC program from the end of the “then” and “else” branches of a compiled if-conditional.
It works only for epilogue step forms (see Section 5.5.2).
It is inductive in that it asserts closedness of over pairwise reachability from the pair currently under consideration – the only case to do so directly.
- •
while_expr: This case relates the While program ()’s initial intermediate step to , and its expression evaluation part, with the expression evaluation and conditional jump of the RISC program that was compiled to by .
It relies on being related by to its compiled RISC counterpart when started with initialisation states judged valid by .
- •
while_inner: This case relates some program reachable from to the loop body part of the RISC program compiled from .
It relies on being related by to its compiled RISC counterpart at the appropriate program counter offset.
It also carries around the same reliance on being related by to its compiled RISC counterpart for all initialisation states judged valid by .
- •
while_loop: This case handles epilogue steps for the inner loop body program, and the final jump back to the beginning of the While-loop.
It requires to relate the terminated While program to the end of the compiled loop body, and furthermore also carries around the same reliance on being related by to its compiled RISC counterpart for all initialisation states judged valid by .
Appendix B Code listing for the case of for if-conditionals
This code listing has been adapted slightly to improve the clarity of the presentation. denotes the subset of mappings on which and agree.
compile_cmd C l nl (If e c1 c2) =
(let (Pe, r, C1, faile) = (compile_expr C {} l e);
(br, nl’) = (nl, Suc nl); (ex, nl”) = (nl’, Suc nl’);
(P1, l1, nl1, C2, fail1) = (compile_cmd C1 None nl” c1);
(P2, l2, nl2, C3, fail2) = (compile_cmd C1 (Some br) nl1 c2);
(* Pre-compilation check ensures asmrec C2 = asmrec C3 *)
C’ = (regrec C2 $\sqcap_{R}$ regrec C3, asmrec C2)
in (P*e* @ [((if P*e* = [] then l else None, Jz br r), C1)] @
P1 @ [((l1, Jmp ex), C2)] @ P2 @ [((l2, Nop’), C3)],
Some ex, nl2, C’, fail*e* $\lor$ fail1 $\lor$ fail2))
Appendix C Proof sketch for decomposition principle soundness result
Theorem C.1** (Soundness of ).**
[TABLE]
Proof C.2**.**
The only obligation for (2.6) not obtained immediately from (3.1) is the cube-shaped (Figure 1).
The front face of the cube is just ordinary square-shaped refinement preservation (depicted in 4(a)), given to us by . This gives us that a single concrete step from is simulated by abstract steps , where is given by .
We are then obliged to prove a simulation in the other direction (the back face of the cube), that abstract steps from all configurations related by to are simulated by some concrete step from related by to and by to .
Here, we lean on the determinism of the abstract program’s evaluation semantics (required by the theory) to flip the direction of simulation, knowing that abstract steps from , simulating a single concrete step from , could only be the very same abstract steps from that we were required to consider. This allows us to use once again the square-shaped refinement preservation (4(a)) given to us by .
Consistency of refinement pacing and stopping behaviour (depicted in 4(b)) given by (3.2) then respectively ensure that (via ) is the correct number of abstract steps to consider, and that there will indeed be a concrete step from to drive the matching simulation step.
Finally, the remainder of (depicted in 4(c)) discharges the requirement of closedness and modes-equality maintenance of under lockstep execution, demanded by the bottom face of the cube.
Appendix D More details on the Covern wr-compiler
D.1 Register allocation scheme model
We model the (user-supplied) register allocation scheme by two functions and on the register record (see Section 5.4) and the set of registers whose contents are needed to evaluate the current expression. In order to avoid loading from memory unnecessarily, the compiler may first call to identify a register that records as already containing the variable . When the compiler needs a fresh register, it will call . Neither function is allowed to allocate a register in , so the allocator is permitted to fail if it cannot find any suitable register. As mentioned in Section 5.2 we assume there are enough registers to service the expressions in the source program. Also, registers typically become available again as expression evaluation is resolved.
D.2 Label allocation and sequential composability
For allocating natural numbers to use as labels for RISC instructions the wr-compiler ensures freshness merely by using the highest number reached so far on a “next label” counter ( in the invocation example (1)), incrementing the counter before passing it along to subsequent calls, and outputting the next available unused label on return (as in the example).
We define two RISC programs to be if they are both:
- •
: only ever jumps to labels that are either
- –
labelling an instruction in itself, or
- –
the label of the very first instruction in .
- •
: does not jump to any of the labels of instructions in .
We prove a lemma that says that two RISC programs that were compiled by the wr-compiler consecutively—in the sense that the relevant outputs from the first call are fed directly into the second call—are .
D.3 More detail on and the wr-compiler proofs
The first two requirements to the predicate were given in Section 5.4. Its other two requirements reflect that the terminated While program stop has no valid compilation, and that the initial label (if provided) must be valid (see Section D.2 for more information on label allocation).
Definition D.1** (Requirements on inputs to ).**
[TABLE]
These input conditions give us enough information to prove that every instruction of a -annotated RISC program output by a successful run of is annotated by a stable register record, and that the output ’s register record is also stable:
Lemma D.2** (Successful compilations output only stable register records).**
[TABLE]
Proof D.3**.**
By induction on the structure of the While language program , making reference to the implementation of . For cases that must compile expressions, we furthermore prove and make use of a lemma by induction on the structure of expressions, making reference to the implementation of the expression compiler function called by . In essence, we prove that (sub)expressions that appear in register records must be stable, for two reasons. Firstly, they are always only ever subexpressions over variables that must have been stable in the input program when their contents were first loaded into registers. Furthermore, when compiling an ), the wr-compiler will always flush all register records that make reference to any variables that the ) makes unstable.
Before proceeding, we name the parts of more explicitly:
Definition D.4** (Configuration consistency requirements for compiled commands).**
[TABLE]
Definition D.5** (Consistency between a register record, register bank, and shared memory).**
[TABLE]
Definition D.6** (Consistency between an assumption record and a mode state).**
[TABLE]
Lemma D.7** ( preserves modes and memory).**
**
Proof D.8**.**
By induction on the structure of . For all cases of , is either asserted directly by the guards or obtainable from the inductive hypothesis.
Lemma D.9** ( is closed under changes by others).**
**
Proof D.10**.**
By induction on the structure of . Changes by others (2.5) only modify variables the same way for both configurations, so preservation of is immediate. Also, is unaffected because only creates records (referring to no variables). No other guards mention shared memory.
Lemma D.11** (Successfully compiled programs maintain config consistency requirements).**
[TABLE]
Proof D.12**.**
We in fact prove it separately for and , in both cases by induction on the structure of the While program . In each case, we use the simplifiers for the implementation to yield the corresponding RISC program fragment in question, and then prove the lemma for each of the possible locations of in the compiled program. For both proofs, there is some trickiness in accounting for (and ruling out) which destination must be considered for each of these cases of , particularly for those While programs that compile to RISC programs that may have jumps in them.
Control flow trickiness aside, the intuition for is that it tests the correctness of the compilation of expressions, and so for this we must prove a sub-lemma for maintenance of by induction on the structure of expressions that are encountered in the While programs . Additionally, flushes register record entries mentioning variables that are to become unstable, and conservatively flushes entries to force evaluation of the loop condition expression. This is safe trivially because flushing entries can never make a consistent register record inconsistent. The rest of the cases for are straightforward because they do not touch the register record.
Then for , the substantial part of the proof is as a test of the correctness of the compiler’s bookkeeping of assumptions being consistent with the semantics of and . The other cases for do not touch the mode state.
Lemma D.13** (Correctness of the expression compiler).**
[TABLE]
Proof D.14**.**
By induction on the structure of expressions , using the simplification rules for the implementation of , and also relying on assumptions of correctness of the register allocation scheme supplied by the instantiator of the theory.
Lemma D.15** ( is a refinement paced by ).**
[TABLE]
Proof D.16**.**
By induction on the structure of .
The base case stop is immediate, because it pertains to a terminated While and RISC program. The base cases that proceed in one step to a terminating program configuration (skip_nop, assign_store, lock_acq, lock_rel) are fairly straightforward because after dealing with the single step, the resulting obligation can then be handled by the stop case. This leaves the last remaining base case assign_expr, which proceeds in one step either to itself, or to assign_store. In all of these cases, we use D.11 to obtain the preservation of the guards demanded by the introduction rule for the destination configuration of the step. Particularly, the assign_store case must make use of and the correctness of (D.13) in order to ensure that once the expression evaluation result is written back to shared memory, holds as demanded by the stop case.
*The inductive cases that concern expression evaluation (if_expr, while_expr) are much like assign_expr in that they have the possibility of progressing in one step to themselves. Unlike assign_expr however, their other possibility is a conditional jump based on the result of that expression. Again we use D.13 to obtain that the result is an accurate calculation of the expression, and this time we prove by the two different cases whether if_expr ends up in if_c1 or if_c2, or if while_expr ends up in while_inner or at stop (having jumped to the exit label). In these cases, the guards over which the inductive references to have been quantified are versatile enough to discharge themselves (when _expr steps to itself), or to discharge any reachable initial starting state for the nested compiled RISC program, given that D.11 ensures the invariance of these guards.
This just leaves the inductive cases that pertain to configurations inside a nested compiled RISC program (if_c1, if_c2, while_inner), or at the end of one (epilogue_step, while_loop). In these cases, the inductive hypotheses obtained from the inductive reference to are always enough to satisfy the guards demanded by the possible destination cases. Like in the proof of D.11, the trickiness mostly comes from accounting for all the possible cases of control flow (ruling out spurious destinations) that need to be considered.
Lemma D.17**.**
**
Proof D.18**.**
3.2* gives us the following obligations.*
For consistent stopping behaviour, we prove a lemma that RISC programs stop if and only if their is outside the program text , i.e. . Because equates and for the two configurations, then clearly both have identical stopping behaviour.
For consistency of change in timing behaviour, depends only on While and RISC program locations, and and forces them (resp.) to be equal for the local configurations under consideration.
For closedness of under lockstep execution, the only non-straightforward cases to consider are conditional branching, and the locking primitives. For conditional branching, we use for with memory preservation via (5.2) to ensure that the conditional branching outcome is the same on both sides.
Finally, as the only operations that touch mode state, the locking primitives are the only non-straightforward cases for mode state equality maintenance under lockstep execution. As all lock memory is classified (see Section 5.3), we use for with memory preservation via to ensure the RISC configurations behave consistently.
Lemma D.19**.**
**
Proof D.20**.**
Referring to 3.1, the obligations pertaining only to and are discharged by 5.5, 5.3, and 5.2. Pertaining to : clearly is symmetric, and furthermore it is (2.3) because the actions over which must be closed modify only the shared memory, and places only restrictions on the program text and current location. The final obligation is discharged by D.17.
Theorem D.21** (Successful compilations are refinements in ).**
[TABLE]
Proof D.22**.**
By induction on the structure of While. The compiler input and initial configuration conditions we impose allow us to have each of skip, , , , , , and and their compiled output meet the guards of the introduction rules for the cases skip, seq, if_expr, while_expr, assign_expr, lock_acq, and lock_rel of that were designed for them respectively.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault. Exploring robust property preservation for secure compilation. Co RR , abs/1807.04603, 2018. URL: http://arxiv.org/abs/1807.04603 .
- 2[2] G. Barthe, B. Grégoire, and V. Laporte. Secure compilation of side-channel countermeasures: The case of cryptographic “constant-time”. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF) , pages 328–343, July 2018.
- 3[3] Gilles Barthe, Tamara Rezk, and Amitabh Basu. Security types preserving compilation. Comput. Lang. Syst. Struct. , 33(2):35–59, July 2007. URL: http://dx.doi.org/10.1016/j.cl.2005.05.002 . · doi ↗
- 4[4] Gilles Barthe, Tamara Rezk, Alejandro Russo, and Andrei Sabelfeld. Security of multithreaded programs by compilation. ACM Trans. Inf. Syst. Secur. , 13(3):21:1–21:32, July 2010. URL: http://doi.acm.org/10.1145/1805974.1805977 .
- 5[5] Mark Beaumont, Jim Mc Carthy, and Toby Murray. The cross domain desktop compositor: Using hardware-based video compositing for a multi-level secure user interface. In Annual Computer Security Applications Conference (ACSAC) , pages 533–545, 2016.
- 6[6] Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur. , 18(6):1157–1210, September 2010. URL: http://dl.acm.org/citation.cfm?id=1891823.1891830 .
- 7[7] Florian Dewald, Heiko Mantel, and Alexandra Weber. AVR processors as a platform for language-based security. In Computer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I , pages 427–445, 2017. URL: https://doi.org/10.1007/978-3-319-66402-6_25 . · doi ↗
- 8[8] Qian Ge, Yuval Yarom, Tom Chothia, and Gernot Heiser. Time protection: the missing OS abstraction. In Eurosys 19 , Dresden, Germany, March 2019. ACM.