The Defense Advanced Research Projects Agency (DARPA) has awarded a $1.8 million contract jointly to two companies – Galois, a Portland-based computer science company, and Guardtime Federal, a cyber-security provider – to advance the state of formal verification tools and all blockchain-based integrity monitoring systems.

The companies will verify the correctness of Guardtime Federal’s Keyless Signature Infrastructure (KSI) – a blockchain technology that provides massive scale data authentication without reliance on centralized trust authorities.

“Formal verification has evolved considerably over the past several years, but has only recently matured enough to tackle production-level software,” said Stephen Magill, Research Lead for Software Analysis at Galois. “This collaborative effort seeks to advance our understanding of the role that integrity analysis plays in system security and lead to improvements in formal verification tools and methods that will be applicable to other existing systems.”

Galois is a leader in formal verification, a technique that goes beyond testing and evaluation to provide mathematical assurances that a system works only as intended in all cases. Verifying the correctness of Guardtime Federal’s KSI will demonstrate the scalability and practicality of formal verification methods as a means for establishing trust in critical systems.

Integrity monitoring systems like Guardtime Federal’s KSI detect evidence of Advanced Persistent Threats (APTs) as they work to remain hidden in networks. APTs, which have been central in many major network breaches, undermine network security, cover their tracks by removing evidence from system log files, add information to “white-lists” used by security software, and alter network configurations. This project aims to verify the ability of keyless integrity monitoring systems to detect APTs and attest to the ongoing integrity of a system.

“Guardtime Federal sees this formal verification of block chain and keyless infrastructure technology implemented to meet national security challenges as an amazing opportunity for our clients,” said David Hamilton, President of Guardtime Federal. “By subjecting our cyber defense infrastructure to this most sophisticated methodology we will test both typical and exotic boundary conditions enabling further refinements of our defenses for protecting the most precious national security secrets and configurations of operational systems.”

Technology such as Guardtime’s KSI can be used to ensure intruders are unable to cover their tracks. Formal verification aims to provide mathematically grounded assurance that the KSI system will not be compromised no matter what the intruder does to subvert it.

In July, Galois was awarded a $6 million contract under a DARPA program to develop a system to detect APT cyber attacks in increasingly complex enterprise network and system environments.