History for Secure Flow Checking

changed:
-
Verified secure flow checker

  Barthe and Rezk (TLDI 2005) give an iterative analysis for determining a security labeling bytecode with respect to a given security policy for a program's public API. Here a policy consists of assignment of levels in a lattice to the public methods, fields and global variables. The analysis has been proved sound in the sense that accepted programs are noninterferent in accord with the policy, where noninterference means absence of influence in terms of a standard semantics in which timing, power consumption,
resource exhaustion and othe covert channels are not modeled.  
For bytecode generated by a compiler, the compiler can produce this labeling; the analysis has been simplified for use in that case.

  **Challenge:**
Give a machine-checked proof of noninterference for the revised system. This involves a semantics for bytecode, specification of the analysis, quantification over all programs, and the noninterference property which has the form of a logical relation or simulation (property of not one but two executions).

  If the analysis is specified in a form that is executable, such as the functional program in Naumann's verification of a source level checker in PVS~\cite{naumann-tphols05}, then this could be considered a verified program rather than verified meta-theory.  
But for practical deployment an implementation would at least need glue code in addition to the pure PVS functions; most likely a bytecode checker for production use will be implemented in a subset of C, possibly compiled with optimizations or linked with hand written assembler.  

  **Challenge:**
Verify an implementation of this analysis with respect to its full functional specification, i.e., accepted bytecode is noninterferent.
The obvious proof strategy would be to rely on the noninterference result for an abstract description of the analysis (previous challenge item): prove that the implementation simulates the abstract program in a suitable sense.  
This involves semantics of both the implementation language and the
``specification language'' in which the abstract program is expressed. An alternative to carrying out the simulation proof directly in terms of the semantics would be a more ``axiomatic'' approach; e.g., using an assertion-based program logic (in which components of the abstract program might be admissible
as terms), or using equivalence preserving transformations.

  An input to the bytecode analysis is a sound approximation of the program's control dependence regions (to track flow of information via control flow). An implementation of the analysis should include a check that the regions are correct (a high level implementation has been machine checked in Coq by Barthe). But regions are used for other purposes, in particular, optimizing transformations.  
The challenge can be embellished by including optimization and asking that the region analysis be treated as a component so, in particular, its specification is sufficiently strong and general to cater for these multiple purposes.

  Bytecode optimization also entails adapting the security analysis.  Can verification of the original analysis be adapted to one that handles some important optimizations?  Or to an algorithm for finding regions and finding security labeling?  Can the properties proved be re-used, or the proof techniques and ancillary results?

  Finally, the bytecode labeling is produced by the compiler based on information from a source level analysis.  Security of the bytecode does not depend on correctess of the compiler but it is desirable that source code deemed secure by the source level analysis compiles to bytecode that is accepted. This has been proved on paper via a slightly intricate technique which the authors claim can be used to cater for additional language features and more
sophisticated security policies.

  **Challenge:**
Formulate the source level analysis and label-generating compiler.  
Machine-check a proof that accepted source code compiles to accepted bytecode. Extend the language and policies; adapt the proof.

  **Challenge:**
Extend this to certifying compilation.

   Type based specification of secure flow policy does not adapt easily to various policies involving declassification.  These may be best expressed in terms of assertion-based specifications.  A challenge is to formalize and validate a system integrating both approaches.