Codehawk

Making Software Safer


Sound

CodeHawk applies abstract interpretation techniques to achieve sound results, applying over-approximation to guarantee never missing a property violation.

Scalable

Using divide-and-conquer methods CodeHawk can scale easily to large code targets, and can reuse previous results on subsequent runs to minimize rework.

Flexible

One analysis engine works on verification of many source languages, and can be used in binary reverse engineering tasks. Using multiple abstract domains the engine supports a variety of analysis problems and properties.

Presentations

See our product fliers, white papers, and other presentation files at  SlideShare

KT CodeHawk Technology

Our abstract interpretation engine is named CodeHawk. It is the core technology inside each of our analyzers.

The CodeHawk engine applies abstract interpretation techniques by implementing a number of iterators and abstract analysis domains. The analysis domains include

  • constants
  • intervals
  • strided intervals
  • linear equalities
  • polyhedra
  • symbolic sets
  • value sets, and
  • taint

To provide isolation from the input language CodeHawk has its own internal form. This design enables CodeHawk to accommodate a number of different front-ends from different input languages. We currently offer front-ends for C, Java byte code, and X86PE binary.

codehawk
placehold

KT Advance

KT Advance is our C-language analyzer, a verification product designed specifically for memory safety properties. The analyzer has built-in knowledge of the C specification, specifically the undefined behaviors that can lead to weaknesses, which it embodies in a collection of memory safety properties. Using CodeHawk as its analysis engine, the analyzer transforms the C source into the CodeHawk internal analysis form. It produces proof obligations for every line of the program based on our property descriptions for the memory safety properties. It then uses 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. We provide a Python API for scriptable access to these results. We also provide plugins for Eclipse CDT, the Atom editor, and for SonarQube.

KT Transferal

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 XML results. We also provide a plugin for integration with the IDA Pro tool platform.

logo

trybuy

Buy or Try Our Analyzers

We provide our analyzers by subscription. Buy a subscription by the month or by the year, using it when you need to suit your activity level or development lifecycle. The online subscription site will be available soon; in the meantime contact our sales office to obtain a license.

Oftentimes potential users are interested in evaluating our analyzers for verification or reverse engineering results but are unsure of platform compatibility, workflow integrations, runtime performance, or other concerns. Others want to develop proprietary feature additions, to integrate custom user interfaces, or to develop feature requirements for us to implement in future editions. For these reasons we can provide evaluation licenses for the runtime products, and we are willing to license our IP for proprietary integrations or product development.

Contact Us

About Us

Learn more about the company's technology and motivating pursuits.

More...

Contact

  +1.650.320.8474