Exploit Generation tool – KEG
KeY Exploit Generation (KEG) tool allows to analyse Java programs for information-flow leaks (violation of a specified information-flow policy) and generates exploits for found information leaks.
It uses KeY, a state-of-the-art theorem prover for Java as symbolic execution and verification engine. Since version 0.1.2, KEG supports secret inference simulation. It enables users to run insecure programs multiple times with unknown yet fixed high input (secret) and optimal low input (generated by KEG) to infer the value of secret. It brings a comprehensive view about the severity of information leaks. Currently, it supports:
- Policies: non-interference and target conditional delimited release as declassification.
- Arithmetic: Interger arithmetic (addition, subtraction, multiplication, division, modulo)
- Java properties: objects, arrays (partly supported), unbounded loop (using loop invariant), recursive method call (using method contract)
- Java SE 1.7 or higher
- JUnit framework to run JUnit test (optional, needed to run JUnit test generated automatically by KEG incase information leaks are detected)
Download and Install
Download z3 for Java. You can build z3 for Java by yourself here
Extract the compressed file into an accessible directory (KEG's folder). All jar files must be in the same folder. For example, you can extract all jar file into folder “C:\exploitgen” and make sure that accessing folder exploitgen is allowed by the operating system.
Extract and copy all files in z3 for Java folder into KEG's folder. Append the path of KEG's folder to environment variable PATH. It could be done in command line interface mode in both Windows and Linux
- Windows: setx path “%path%;directoryPath”. For example, if KEG's folder is “C:\exploitgen” then the command is: setx path “%path%;C:\exploitgen”
- Linux: export PATH=$PATH:/directoryPath. For example, if KEG's folder is “/usr/exploitgen” then the command is: export PATH=$PATH:/usr/exploitgen
External tools for secret inferrence
- Counting tool: barvinok. Set the environment variable PATH pointing to the folder containing the executable iscc
- Optimization tools:
- AMPL:. Set PATH pointing to the folder containing the executable ampl
- Bonmin, Couenne: Set PATH pointing to the folder containing the binary files
- LocalSolver: Copy file localsolfer.jar to KEG's folder. Set PATH pointing to the folder containing files liblocalsolver.dll(so/dylib), liblocalsolvernativejava.dll(so/dylib) and license.dat
Open Java program needed be checked and specify information flow security policies for it. A short tutorial how to specify information-flow policies can be found here
Open the command line interface on your computer. Switch to KEG's folder.
Run exploitgen.jar to check the specified program. A full path of target program must be passed as parameter. For example, if you want to check information flow security for the Java program “C:\banking\CheckAccount.java” then the command is:
- java -jar exploitgen.jar C:\banking\CheckAccount.java
Using loop invariant and method contracts: If the interested Java code contains specifications for loop invariant and/or method contracts and you want to use them when checking a program with unbounded loops and/or recursive method calls, you have to supply usage parameters for KEG. For loop invariants, the parameter is -li, while for method contract, the parameter is -mc. For example, if you want to check CheckAccount.java program using loop invariant and method contract, the command can be:
- java -jar exploitgen.jar C:\banking\CheckAccount.java -li -mc
Note: When a jJava file is checked by KEG, all other Java files in the same folder and subfolders are also loaded by KeY engine in KEG. Therefore all of them must be specified correctly. For example, if you want to check file C:\banking\CheckAccount.java, you have to make sure that all specifications (if they exist) are composed correctly not only in CheckAccount.java but also in all other java files in folder banking and all of its sub-folders, otherwise an exception error will be thrown.
If the Java file is insecure w.r.t. the specification, a JUnit test file is created automatically. Then you can:
- Open it to investigate how and where the secret information can be leaked
- Run it as a normal JUnit test
The JUnit test file will be stored in a subfolder of the parent folder to the one containing the analysed Java file. For example, if file “C:\banking\CheckAccount.java” is insecure, then KEG will create exploits and store it in JUnit test file “C:\testbanking\TestCheckAccount.java”
A set of examples can be downloaded here
E-Voting System (Declassification and Information Erasure)
POST 2016: E-Voting Case Study (Privacy Game)
- Source Code
- Specification generation: KeY IF
- Exploit generation: KEG