Software developed by DeduSec

QIF/SAT and QIF/Poly: Quantitative Information Flow Analysis

Tools for quantitative information flow analysis of imperative programs developed within DeduSec are available here.

Entroposcope: Static Analysis for PRNGs

Entroposcope is the first static analysis for finding defects in PRNGs. The tool was used to find the long-escaping PRNG bug in the GnuPG/Libgcrypt PRNG (CVE-2016-6313).

Rêve: Automatic CEGAR-based Information Flow Analysis

The Rêve tool was originally developed by our group within the IMPROVE/SPP 1593 project to automatically check two C-like programs for equivalence. The version of the tool linked above demonstrates that the same techniques can be used for checking automatically and with high precision for absence of illicit information flow. Relaxation such as declassification can be easily treated in the same framework.

SemSlice

SemSlice is a slicer that uses Rêve to determine whether a slice candidate is indeed a correct slice. The tool also provides three strategies for generating slice candidates.

Specifying and Verifying Information Flow in Object-oriented Programs with KeY

KeY is an interactive/automated theorem prover for reasoning about behavior of Java programs in Dynamic Logic. Verification of information flow properties is now included in KeY 2.4. It is available via web start (link in box on the right).

How to read the JML information flow specifications?

We use an extension of JML to specify information flow on the program level. The main concept behind the extension is the usage of information flow (method or block) contracts. Those contracts mainly consist of (1) a precondition, (2) a list of low expressions for the pre-state and (3) a list of low expressions for the post-state. The contract

/*@ requires x > 0 && y > 0;
  @ determines sum, prod \by x, y, z;
  @*/
void m();

for instance states that the values of sum and prod after the execution of m() depend at most on the initial values of x, y and z — under the condition that x and y are greater than 0 in the initial state.

The \declassifies and \erases parts which can occur in the determines clauses are only syntactic sugar: everything that is listed behind the \declassifies keyword could also be added to the list behind the \by keyword instead. Similarly, everything that is listed behind the \erases keyword could also be added to the list directly behind the determines keyword instead. For object oriented information flow reasoning (objects have to be equivalent up to an isomorphism only), all newly created objects which occur in a determines clause have to be listed behind a \new_objects keyword.

How to use KeY to prove information flow?

After loading an information flow example, activating the "normal" auto-mode by clicking on the "play button" works only for (very) simple problems. In order to start an auto-mode with optimised self-composition reasoning, proceed as follows: (1) highlight an arbitrary term, then (2) left-click, (3) choose the menu item "Strategy macros" and (4) choose in the upcoming menu the item "Full Information Flow Auto Pilot". KeY should prove the example fully automatically now.

What to do if the auto pilot fails?

If the auto pilot fails (which might be the case for complicated examples), one has to perform the following steps in order to be able to interact with KeY.

Self-composition considers the same program twice with different variable names, but it suffices to calculate only one weakest precondition and do the renaming directly on the thus calculated formula. Therefore one has to start a side-proof for the weakest precondition calculation. This is done as follows:

(1) Highlight an arbitrary term and left-click.

(2) Choose the menu item "Strategy macros" and in the upcoming menu the item "Auxiliary Computation Auto Pilot". Then a side proof will be opened and KeY will try to automatically calculate the weakest precondition. KeY succeeded in the calculation if the remaining open goals of the side proof do not contain modalities any more. If a goal still contains a modality, then one can either simply try to increase the number of auto-mode steps or one can remove the modalities by interactive steps. If one of the open goals contains an information flow proof obligation from a block contract or from an information flow loop invariant, then this goal has to be closed by going through steps (1) to (5) again before continuing with step (3).

(3) Choose one of the open goals. Highlight something in the sequent and left-click.

(4) Choose the menu item "Strategy macros" and in the upcoming menu the item "Finish auxiliary computation". The side proof will be closed and a new taclet (rule) will be introduced to the main proof which is able to replace the self-composition term (the shortest term which contains both modalities) by two instantiations of the calculated formula.

(5) On simple examples it suffices now to click on the play button (activate the auto mode). On more complex examples it is helpful to run the strategy macro "self-composition state expansion with inf flow contracts" first.

The macro "Full Information Flow Auto Pilot" applies steps (1)-(5) automatically.

Combining KeY with JOANA

The goal of this project is to create a solution which combines system dependency graph analysis (using JOANA) with deductive verification (using KeY) to analyze Information flow in programs.