Our Company
Kestrel Technology (KT) is a research and development company located in Palo Alto, CA. KT is staffed by highly trained computer scientists, mathematicians, and engineers who share a vision for using sound mathematical foundations for assuring the highest level of software robustness, reliability and security.
Our Mission
Our mission is to develop software analysis tools that provide automated mathematical assurance of software correctness in a cost effective way, and to apply them to real world applications.
In particular, KT has developed technology that can automatically prove the absence of targeted security vulnerabilities in software. The technology currently analyzes C source code with projects underway that extend the analysis capability to binary and Java byte code.
Our “Next Generation” Software Analysis Tool: CodeHawk
KT has developed a very high precision, automated, customizable and tunable static source code analyzer called CodeHawk. For the first time, code developers and testers can use a low cost, automated tool to prove software correctness. For example, CodeHawk has been applied to a variety of open source C programs, to automatically measure the safety level of the code for key security vulnerabilities, such as buffer overflows.
Codehawk is a highly engineered tool that aims for sound analysis and can reason about properties over infinite domains. It performs an exhaustive check on all code locations that could possibly violate the property of interest and produces mathematical evidence of safety for all these locations, thus enabling a third-party check of the analysis results.
Our Value Proposition to Customers
For certain security vulnerabilities, CodeHawk can automatically measure in minutes and supply proof-based evidence of software correctness. For customers doing security code review to verify the absence of security vulnerabilities in their code, Codehawk is a powerful productivity tool. It can dramatically reduce the amount of code needed to be reviewed, by automatically proving the safety of large segments of the code with respect to the targeted security properties.
Ideal Target Solutions for CodeHawk
- Analyzing C source code to automatically prove the absence of targeted security vulnerabilities to minimize the amount of code remaining for manual security code review
- Hardening of C source code against specific targeted vulnerabilities by using CodeHawk vulnerability boundaries
Partnering with Kestrel Technology
We seek:
- Government agencies interested in funding research to make "sound" static analysis practical for real applications for analyzing binary code, Java bytecode or C source code
- Commercial entities interested in commercial partnerships for developing "next-generation" products or services utilizing "sound" static analysis for analyzing binary code, Java bytecode or C source code
- End user customers interested in evaluating the CodeHawk C source code tool to increase the productivity of their security review process for verifying the absence of key security vulnerabilities in their C source code
- Customers interested in evaluating binary code. CodeHawk provides additional information complimentary to IDA Pro to help in identifying vulnerabilities
