Kestrel Technology (KT) specializes in sound static analysis with applications in software security, reliability, and robustness. Our core technology is abstract interpretation-a technology that can, for example, look at program structure to understand the root cause of memory weaknesses and provide mathematical proof-based (instead of heuristic-based) assurance of the absence of memory vulnerabilities. The technology is implemented in our highly optimized, scalable, language-independent abstract-interpretation engine-called CodeHawk.
Our mission is to leverage our core technology of abstract interpretation to develop more accurate and efficient static software analysis tools.
Our “Next Generation” Software Analysis Tool: CodeHawk
KT has developed a very high precision, scalable, automated, customizable and tunable static code analyzer called CodeHawk. The language-independent analysis engine supports three front-ends: C source code, Java byte code and Binary. The CodeHawk C analyzer is targeted at mathematically proving the absence of memory access vulnerabilities in C programs (e.g. preventing Heartbleed type attacks). The CodeHawk binary analyzer is targeted at providing large amounts of semantic data in xml format about a binary executable and providing assistance in the identification of potentially exploitable memory access violations. The CodeHawk Java analyzer tracks taint and provides assistance in identifying resource handling and synchronization problems.
Our Value Proposition to Customers
For C code memory vulnerabilities, such as buffer overflows, CodeHawk can automatically analyze C programs in minutes and supply proof-based mathematical evidence of the safety of memory accesses in the code. The C analyzer is being developed to be integrated into the development process (e.g. as an Eclipse IDE plug-in) and guarantee memory safety throughout the process resulting in the delivery of much more secure software products that prevent zero day attacks targeting memory vulnerabilities. The analyzer can also be developed to be integrated into test centers (e.g. SWAMP) and automatically verify the memory safety of critical legacy proprietary and open source C code to prevent costly zero day attacks on memory vulnerabilities like the recent Heartbleed attack.
For binary code, CodeHawk can dramatically reduce the time required for reverse engineering of the code by largely automating the process. A C++ inquiry tool allows access to large amounts of xml formatted semantic data on variables, arguments, register values, stack pointers, predicates and loops. Its understanding of program structure provides the capability to develop a tool that can automatically prioritize potential memory vulnerabilities in x86 executables by ease of exploitability and severity, and provide test inputs to confirm the exploitability of the potential vulnerability (e.g. automatically generate counterexamples).
Ideal Target Solutions for CodeHawk
- Integrate the technology into the development cycle for C source code to automatically prove with mathematical evidence the absence of memory vulnerabilities to guarantee the code is safe from zero day attacks on memory vulnerabilities
- Integrate the technology into test centers such that legacy C program memory accesses can be proved with mathematical evidence to be 100% safe and guarantee the code is safe from zero day attacks on memory vulnerabilities
- Integrate the technology with disassemblers (e.g. IDA Pro) so IDA disassembly results can be merged with CodeHawk results for x86 analysis and analysis results can be displayed in IDA GIU
- Integrate the technology with dynamic analysis tools to allow much more targeted dynamic analysis based on CodeHawk analysis results
- Integrate the technology with malware / forensic tools to allow much more targeted analysis based on CodeHawk analysis results
- Integrate the technology into test centers such that legacy executables can be analyzed for memory vulnerabilities
Partnering with Kestrel Technology
- Customers interested in being alpha / beta test sites for the to be developed C analyzer and Binary analyzer products
- Government agencies / commercial partners interested in funding KT to develop the CodeHawk technology to fit their V&V and security testing needs