CONTACT | Epistemic Noninterference COncolic VERifier |
At a glance |
ENCoVer addresses the problem of program verification for information flow policies by means of symbolic execution and model checking. Noninterference-like security policies are formalized using epistemic logic. A related paper (see bottom of page) shows how the policies can be accurately verified using a combination of concolic testing and SMT solving. As demonstrated, many scenarios considered tricky in the literature can be solved precisely using the proposed approach. This is confirmed by experiments performed with ENCoVer, a tool based on Java PathFinder and Z3, which we have developed for epistemic noninterference concolic verification.
The theory presented in the related paper has been implemented in a prototype called ENCoVer. For the extraction of the symbolic output tree (SOT) from Java bytecode, ENCoVer relies on Symbolic PathFinder (SPF), an extension of Java PathFinder. SPF exercises all possible execution paths of the analyzed program by means of concolic testing. During this phase, SPF computes and maintains symbolic expressions representative of the current path condition and of the value of every variable for the current path under test. Whenever a statement rendering a value “observable” is executed, ENCoVer creates a new node in the SOT under generation using the symbolic expressions corresponding to this observable value and the current path condition. After this first phase corresponding to the SOT generation, ENCoVer converts the SOT into an interference formula (f) with free variables. This formula, with its free variables existentially quantified, is the negation of the noninterference formula applied to the program analyzed. Any assignment to the free variables that renders the formula f true is a counterexample proving that the program is not noninterfering. Finally, ENCoVer feeds the formula f to a satisfiability modulo theory (SMT) solver (Z3 in the current implementation). If the SMT solver answers that the formula is unsatisfiable, then the analyzed program is deemed noninterfering. Otherwise the program is declared interfering, and the assignment provided by the SMT solver is returned as a counterexample of the noninterference behavior of the analyzed program. ENCoVer has been implemented in Java as an extension of Java PathFinder (JPF). The extension by itself has 86 classes/interfaces and 6 KLOC as computed by CLOC, and 161 KLOC including the required parts of SPF. The class of programs that the current implementation of ENCoVer can handle is indirectly limited by the class of programs SPF (JPF core and its symbc extension) can handle and the class of expressions Z3 can solve. There is no intrinsic limitation induced by the specifics of ENCoVer itself. Theoretically SPF can execute any Java bytecode, however in practice SPF is limited by missing implementations for some native libraries (such as java.io and java.net), a few bugs (such as NullPointer exceptions being reported as NoSuchMethod exceptions), and of course state space explosion (particularly when dealing with multithreaded programs with loose synchronization constraints). In the current implementation (due to the way SPF handles booleans, and differences between SPF expressions and Z3 expressions that requires typing in order to translate from one to the other), ENCoVer is limited to the manipulation of integer expressions as described by the Core and Ints theories of SMT-LIB standard. Z3 can solve a fair number of formulas based on those expressions. In the future, the class of programs handled by ENCoVer should grow due to continuous development on SPF and Z3. |
The current release is a prototype. There are known bugs here and there, however non-trivial examples can still be handled.
Installation and testing process has been simplified for Unix systems and is explained step by step in a file README.src contained in the zip file containing ENCoVer sources. For OSX systems, the same process should work. For Windows systems, some small modifications (mainly creating .bat files corresponding to 2 Bash scripts used) are necessary.
In short, you need to:
ENCoVer is distributed under the terms of the GPL v3 license, except for some third party softwares or libraries. ENCoVer embeds different libraries with different licenses. Those unmodified libraries are dynamically linked at run-time. Those libraries can be found in the ENCoVer source or binary zip files in the "lib" directory.
Those third party softwares or libraries are:
1. Musard Balliu, Mads Dam, and Gurvan Le Guernic. ENCOVER: Symbolic Exploration for Information Flow Security. In Proceedings of the IEEE Computer Security Foundations Symposium. Harvard, MA, USA. June 2012.
@INPROCEEDINGS{bdlg12encover,
author = "Balliu, Musard and Dam, Mads and Le Guernic, Gurvan",
title = "{ENCoVer}: {S}ymbolic {E}xploration for {I}nformation {F}low {S}ecurity",
booktitle = "Proceedings of the IEEE Computer Security Foundations Symposium",
year = 2012,
month = jun,
}
2. Musard Balliu and Mads Dam and Gurvan Le Guernic. Epistemic Temporal Logic for Information Flow Security . In the Proc.of ACM SIGPLAN Programming Languages and Analysis for Security (PLAS '11 ). San Jose, CA, USA. June 5, 2011.
@INPROCEEDINGS{bdlg11etl4ifs,
author = "Balliu, Musard and Dam, Mads and Le Guernic, Gurvan",
title = "{E}pistemic {T}emporal {L}ogic for {I}nformation {F}low {S}ecurity",
booktitle = "Proceedings of the ACM SIGPLAN Programming Languages and Analysis for Security”,
year = 2011,
month = jun,
}