An analyzer for Java bytecode, currently relying solely on "brute-force" symbolic execution.
This software has mostly been developed for learning/experimentation purposes. It has demonstrated its ability to find some bugs in example programs (see a toy example here), but it is still very incomplete.
- Intra-method analysis
- Method summaries generation
- Exploit summaries of already analyzed methods
- Track the values in arrays, when not aliased
- Track the values in fields, when field is immutable or object is not aliased (requires to detect at least getters and setters)
- Detect which of its arguments a method can modify
- Support for typestates/protocols
List of resources that are useful to this project:
- A Survey of Symbolic Execution Techniques
- Java ASM bytecode manipulation library, especially the analysis tree API
- KSMT library