About Us, About You

Our Story


Context

When you build software intended to interact with the real world, you want to do a good job. Software in embedded systems, especially in safety-critical systems, must achieve its functional requirements but also be hardened to eliminate a wide range of vulnerabilities. You want to apply comprehensive tests and get the most out of automated software analysis tools. So you want useful software analysis tools; you don't want to be covered up in output that provides no help. With embedded systems continuing to grow, in medical devices, entertainment devices, transportation, internet of things, and many other applications, software analysis needs continue to grow alongside.

When you examine software someone else built to interact with the real world, say for a reverse engineering or malware analysis task, you also want to do a good job. You usually want to do this good job quickly, too. You want automated tools that can extract helpful details, see through obfuscation efforts, and resolve variables and indirections faster than you can on your own. You want an automated tool that understands the semantics of the program, not merely a few clever syntax pattern matches. With malware growing more sophisticated, obfuscation becoming more popular, and efforts proliferating, the increased demand for capacity to analyze malware and quickly obtain indicators of compromise is driving a need for more and better automated analysis methods.

Value

In either software verification or reverse engineering it seems as though there is never enough time. You want tools that you can use right away, with a shallow learning curve, and that provide clear results. In short, you want tools that don't waste your time.

Delivery

Our competitive advantage is in static analysis so that is where we focus our efforts. Our approach to static analysis facilitates verification and reverse engineering activities by revealing the underyling analysis procedures. We show what proof obligations are imposed at each location, what invariants and evidence were obtained and by what proof method, and identify what assumptions must be made to satisfy more obligations. When left with an open proof obligations, you are not left in the dark wondering what the tool was trying to do; all of the analysis information and context is available for inspection at each location. We provide legible output files and APIs for integration, including example scripts for querying results.

What distinguishes our static analysis delivery is our engineering achievement with abstract interpretation technology. Abstract interpretation is a form of program analysis that has been around for a long time, but is difficult to comprehend and implement correctly. Our implementation is embodied in our flagship technology called CodeHawk. Simply put, we think CodeHawk represents the best implementation of abstract interpretation technology you will find anywhere. CodeHawk performs the difficult work of generating invariants for every execution of the program. But while these results are difficult to generate, they are easy to check. We use CodeHawk inside all of our static analysis tools. We invite you to try one of our analysis tools and see for yourself.

In addition to comprehensibility, our engineering achievement addresses the scalability questions as well. The CodeHawk procedure performs program analysis at the function level, considering the global context, and is therefore scalable to large programs. Moreover it accommodates incremental analysis using previous results, so successive analyses run much faster when only a small portion of the program has changed. And because we depend only on static analysis, not dynamic or symbolic analysis, it is not necessary to run the program.

We want to put this analysis capability into your hands, integrated with your tool chains, so you can realize the benefits. The commercial products delivering these capabilities will soon enter the retail marketplace. Already addressing some of your concerns, we adopted a subscription model of license acquisition in order to adapt better to software development lifecycles. With your feedback, we hope to address your priorities immediately and help you make better use of static analysis tools. Alternatively, for your own product development, we will also license the CodeHawk IP for specific applications or markets.

Company

Several years of sponsored R&D work with US Federal agencies especially IARPA, DARPA and DHS, together with our own internal investments, helped us push this CodeHawk technology to the finish line. We still work with Federal agencies today, more on the applied end of R&D than on the basic research end, building new analyzers and integrations for various purposes. We will continue to blend sponsored R&D project efforts with commercial product development for the foreseeable future, one activity informing the other.

“Any sufficiently advanced technology is indistinguishable from magic.”

Clarke's Third Law

Image Title

Our static analysis tool offerings might be summarized as shown here. Our CodeHawk technology provides the abstract interpretation engine for all products. Our current commercial offerings of KT Advance and KT Transferal use this engine to provide static analysis provides for verification and malware analysis, respectively.


KT CodeHawk is our abstract interpretation engine. It performs the abstract interpretation analysis for each of our static analysis products. Several analysis domains already have been implemented such as intervals, value sets, symbolic sets, linear equalities, linear inequalities, taint, and polyhedra. CodeHawk has its own internal form, so it can accommodate a number of different front-ends from different input languages; for example Java byte code or X86PE binary.
KT Advance is our C-language analyzer, a verification product designed for memory safety properties. KT Advance transforms the C source into an internal analysis form. It produces proof obligations for every line of the program based on our property descriptions for the memory safety properties which we derived from the C language standard. It then uses KT CodeHawk as its invariant generator, collecting evidence about the program with respect to the terms in these obligations. The proof obligation checker then determines which obligations have been closed and provides the evidence and method. Another round of proof obligations might be lifted onto the program's API, so that call parameters and return values can become part of the proof discharging steps. These iterations continue until no new invariants are generated and no new proof obligations have been closed. Output goes to XML for integration with tool chains.
KT Transferal is our X86PE binary analyzer, tailored to malware analysis for Windows executables. It provides automated deep semantic analysis of the program, uncovering details hidden by obfuscation efforts. It recovers variables and indirect calls, and reports indicators of compromise as they are found. Successive refinements, working inside-out through memory address resolution, provide incremental results along the way. A Python API provides scriptable interaction with the results. A plugin provides integration with the IDA Pro tool platform.

Company Profile


Spun-off from Kestrel Institute in 2000
Dependable DCAA-compliant teammate
Federal R&D contracts in progress
Silicon Valley HQ location
Open APIs and public repos
Specialists in abstract interpretation