Capybara - An analyzer for Java bytecode

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.

Ideas

• 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

References

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