CodeHawk Overview

KT is developing 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 specific classes of vulnerabilities. CodeHawk achieves very high precision by using a semantic analysis based on Abstract Interpretation technology to calculate invariants at relevant code locations for the targeted vulnerability. The invariants allow mathematical proof of the absence of the vulnerability at that location. CodeHawk is automated and can perform analysis with no input but the code itself. However, CodeHawk can also be customized for code architectures and tuned based on feedback from prior analysis or developer input. The customization and tuning enables an iterative process whereby very high percentages (with a goal of 100%) of the required verification conditions can be proven safe.

How CodeHawk Works

  • CodeHawk attempts to mathematically prove the absence of targeted critical vulnerabilities at all relevant code locations
  • If CodeHawk cannot prove a location is safe for all conditions, a warning is issued. The warning lists the remaining proof obligations, which aids the developer in quickly and inexpensively identifying and resolving the underlying problem
  • An iterative process of analysis and resolving warnings allows developers to produce code in which a high percentage of the relevant code locations are provably free from targeted vulnerabilities
  • As a by-product of this analysis process, CodeHawk generates verifiable evidence of the absence of the vulnerabilities for low cost checking by certifying authorities

Why is Codewak Different?

Existing commercial static analysis tools do not prove the absence of critical vulnerabilities in the code. Instead, they issue warnings that the vulnerabilities may exist at some locations in the code. Resolving these warnings is time consuming and carries the risk of introducing other vulnerabilities (not detected by the tool), because little information is provided on the underlying cause. Existing commercial tools also do not tell the developer what has been checked and how many vulnerabilities have been missed. These tools find bugs, but provide no assurance. In contrast, CodeHawk provides verifiable evidence for all code locations that are proven safe, eliminating the need for manual code review for all of those locations.