Blockchain Technologies

IOG Midnight: ZK Rollups for Secure Scalability

In our latest project, Galois is supporting the launch of IOG’s new data protection blockchain, known as “Midnight.” As part of this effort, Galois is collaborating with IOG to implement recursive zero-knowledge (ZK) proofs in an open-source ZK library called Halo2.

By leveraging zero-knowledge proofs, IOG Midnight ensures that transactions are both correct and private. Implementing recursion enables a technique known as a “ZK Rollups,” which allow transaction proofs to be nested within each other. In other words, verifying the correctness of a proof on one block also verifies the correctness of proofs on all previous blocks in the blockchain. Instead of checking block by block and transaction by transaction to ensure correctness across the chain, users need only check the proof of the latest statement, thus improving efficiency and scalability while maintaining privacy and security.

IOG: Ensuring the Integrity of the Cardano Network

Galois architected the Cardano Network Service Assurance (CNSA) tool to monitor the network at the heart of the Cardano blockchain platform. This robust network-monitoring instrument samples latency statistics across multiple nodes to provide status updates, identify attacks and/or performance degradation, and ensure the network is healthy and operating properly. In addition, Galois implemented networking and ledger code, rigorous property-based testing, and performed code reviews. In combination, these tools and techniques represent a high-assurance ecosystem, bolstering the security and performance of the Cardano network.

Supranational: Securing $15B in Crypto Assets with Formal Verification

In 2020, Galois partnered with Supranational to provide formal verification for ‘blst’, a high-performance cryptography library that helps secure billions (USD) in digital assets, and which serves as an important part of consensus protocols for next-gen blockchain technologies like Eth2 and Filecoin.

For this project, Galois used our Cryptol and SAW toolchain to mathematically prove that the code behaved exactly as expected. Not only did we guarantee the absence of code failures due to undefined behavior in C code—including memory safety violations—but we also showed that the C code exactly met the specification.

Our verification exercise resulted in proofs installed in a continuous integration (CI) environment. These proofs continuously check the code to ensure ongoing validity after each revision, thereby reinforcing its current and future robustness, and rendering ‘blst’ an exemplar for future blockchain technologies and best practices.

Interchain Foundation: Demonstrating the Resilience of the Tendermint Protocol 

Tendermint, the core protocol guaranteeing the integrity of blockchains built on the Tendermint DSK, secures more than 200 projects and an estimated $75B+ in digital tokens. The protocol is a set of communication rules that enable transactions between untrusting parties in a decentralized environment. At the heart of the whole system’s functioning is Tendermint’s Fork-Accountability mechanism, which aims to detect attempts to deviate from the protocol or defraud others, confiscating the deposits of offending parties.

Businesses rely upon the Tendermint protocol and their viability depends on whether their customers trust this technology to secure their assets. Any mistakes in the protocol in general or the Fork-Accountability Mechanism in particular could result in financially and reputationally devastating security breaches.

With these high stakes in mind, the Interchain Foundation asked Galois to put our formal verification expertise to work to ensure that the protocol contained no mistakes. Rather than relying on human intuition or testing inputs, our team of computer scientists built a mathematical model of the protocol and then used logical reasoning and automated proof checking to prove that desirable properties hold once-and-for-all, in all possible scenarios. In this project, our proof demonstrated that, regardless of how many parties collaborate or how clever the attackers are, any parties trying to subvert the financial ledger are guaranteed to be detected and punished.

Stellar Foundation: Security Assurance for Smart Contracts

The blockchain ecosystem has been plagued by security vulnerabilities in recent years, with smart contracts being a prime target for attacks. Every year, billions of dollars worth of digital currencies are lost as hackers exploit even the tiniest of flaws and corner cases hidden deep in the code. Traditional testing methods and auditing tools have proven inadequate, failing to detect exploitable bugs time and time again, resulting in substantial financial losses and diminished trust in blockchain technologies.

Working with the Stellar Foundation to verify Soroban Smart Contracts, Galois built Formal Verso: a Rust front end built on top of our Software Analysis Workbench (SAW), which leverages the power of formal verification to mathematically prove the absence of vulnerabilities in software, covering all possible execution paths, and ensuring that programs behave exactly as intended. This high-assurance tool not only roots out vulnerabilities that are difficult or impossible for traditional testing to catch, but also holds the potential for adaptation across various programming languages, offering a potentially universal solution for securing blockchain technology at large – future-proofing smart contracts against hacks and safeguarding billions in digital currency.

Across our research areas, Galois works to secure critical systems in national security, fintech, and cloud computing applications (including verifying AWS’s cryptographic library) to keep citizens, systems, and data safe; secure financial transactions, and protect the privacy of millions of people across the globe. Now, with Formal Verso, Galois builds upon its established expertise and brings formal verification to the world of smart contracts.

Looking Forward

Shaping the future of blockchain technologies requires pioneering security solutions that you can trust. Galois is here to help.