Runtime Verification is a global leader in software security for the blockchain industry and beyond. The team has developed some of the most advanced and commercially viable formal verification technology and is actively using this technology to raise the safety standard for smart contract systems.
We at IOSG Ventures are thrilled to be leading Runtime Verification’s first fundraising since its establishment in 2010. We will be actively participating in Runtime Verification’s path towards universal verifiable security in the blockchain industry with support on product market fit, talent recruitment, marketing, and business development.
In this article, we are sharing our insights on the unique value of the company’s application of formal verification in the field of blockchain security.
Why does blockchain need security audits?
With blockchain applications booming, the amount of funds locked on the chain has increased exponentially. The security of smart contracts has always been of paramount concern for investors and developers. In 2020, $3.8 billion worth of crypto was stolen in 122 attacks, according to AIthority .
As of June 2021, the TVL of DeFi smart contract has reached more than $52 billion. Loopholes in the code could lead to a great number of financial losses; even more importantly, the project with security incidents may significantly lose its credibility and take a long time, if ever, to regain the trust of users. Nevertheless, despite most DeFi smart contracts having been audited to some degree, all sorts of security incidents still occur regularly. Blockchains and their applications need a much better tool to safeguard their security.
Formal verification is the future of blockchain security?
What is formal verification? What is its advantage?
Formal verification is a revolutionary approach to security, and fundamentally different than traditional security audit. As an example, with formal verification, smart contract code is verified at the bytecode level using tools developed based on a mathematical model of the virtual machine. It proves or otherwise disproves that the code does *just* defined behaviors. This yields a fundamentally much stronger guarantee on the security of the contract code than a process of looking for vulnerabilities, however meticulous the latter process might be.
In the past, it was seen more in the fields of hardware design, embedded system control software, and so on. Because the design cycle in these areas is long, it is difficult to change once it is produced. In addition, many of such systems are mission-critical or could cause life-threatening issues if software flaws are unfortunately triggered. Formal verification enables mathematical models to be built on both the requirements of the system, i.e., what it should do, as well as the system implementation itself. Then it can analyze the security of the system by doing the maths, e.g., proving or disproving mathematical theorems. Compared with manual audits, the security level of formal verification technology is orders of magnitude higher. Because formal verification is based on rigorous mathematical methods, all possible system states are explored and systematically checked for potential exploits.
The core technology of Runtime Verification — the formal semantic framework of programming language K Framework
The background of K Framework
Unlike natural languages which allow interpretation from different angles and even tolerate a certain degree of misunderstanding, programming languages require developers to tell the computer accurate instructions. If there is no strict definition to convey the intent of each program, it is impossible to guarantee a high-reliability and high-security computing system.
“Formal semantics” is an area where computer programming languages are strictly defined. According to the Formal Semantics of Programming Language, it is a discipline in the computer field that uses mathematics as a tool and uses symbols and formulas to accurately define and interpret the semantics of computer programming languages to formalize the semantics.
What are Syntax and Semantics?
Developing the formal semantics of a computer programming language using traditional approaches requires significant mathematical knowledge and is highly complex — most computer language designers do not have the energy and ability to define formal semantics themselves. They often use ad hoc interpreters, compilers, or other manual tools, the consequence of this being that these tools may inadvertently introduce bugs.
Grigore Rosu, Professor of Computer Science at the University of Illinois at Urbana-Champaign (UIUC) and the founder of RV, started developing a set of universal formal semantics for most computer languages when he was working at NASA, prior to joining the UIUC faculty. He believed that if there were no systematic and user-friendly way to formally define the semantics of a programming language, it would be practically infeasible to define and judge whether a program runs correctly.
What is K Framework?
K is a rewrite-based executable semantic framework in which programming languages, type systems, and formal analysis tools can be defined using configurations, computations, and rules. Configurations organize the state in units called cells, which are labeled and can be nested. Computations carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of a program. Computations extend the original language abstract syntax. K (rewrite) rules make it explicit which parts of the term they read-only, write-only, read-write, or do not care about. This makes K suitable for defining truly concurrent languages even in the presence of sharing. Computations are like any other terms in a rewriting environment: they can be matched, moved from one place to another, modified, or deleted. This makes K suitable for defining control-intensive features such as abrupt termination, exceptions, or call/cc.
Now in simpler terms, K allows users to verify software code written in a language chosen (e.g., Solidity) or defined (any customized language) by the user him/herself, rather than restricting the user to program in a very specific programming language just for the sake of formal verification. That is a great benefit for users!
Runtime Verification is becoming the industry standard for blockchain security audits
As early as 2016, Runtime Verification paid close attention to the blockchain industry, and what caught their attention was the DAO attack on Ethereum.
What really established Runtime Verification’s leading position in the security audit in the blockchain industry, especially in the field of the underlying infrastructure, is their in-depth cooperation with the Ethereum Foundation on the security audit of the development of Ethereum 2.0 (developed a formal framework to simulate and verify the Ethereum 2.0 beacon chain protocol, and successfully formalized the finality of Gasper) and the cooperation with IOHK on KEVM and IELE.
Advantages of Runtime Verification compared to other solutions
Runtime Verification vs. other formal verification teams
Runtime Verification combines both the leading academic research capabilities and its broad industry practice experience witnessed by NASA, Toyota, and top blockchain projects.
On the one hand, in terms of security level, the “dynamic verification” of Runtime Verification has a higher safety level than the “static verification” of many other competing products in the market. Compared with other teams that directly verify the source code, Runtime Verification uses the K Framework formal modeling directly on virtual machines such as EVM, so that the deployed bytecode is exactly what is being verified. The verification can verify the program under the actual running environment, which further ensures the safety of the compiler. This is evidenced by its security audit of Ethereum 2.0 beacon chain protocol Gasper and Algorand etc.
On the other hand, Runtime Verification’s K-Framework is more convenient than Coq (used by some other competing products) in terms of tool user-friendliness and automation. Users are free to choose or define whichever programming language to program the logic to be verified.
Nevertheless, like any other areas striving to push the boundaries of scientific innovation, formal verification will only be benefited from competitive efforts from other strong teams as well, such as Certora , CertiK, and Hevm . Especially with the open and community-driven nature of the blockchain space, we believe formal verification’s progress will be accelerated by collaborations among the best teams.
Runtime Verification VS smart contract audit teams (Trail of Bits, Consensys Diligence, Quantstamp, etc.)
Most of the practice today by blockchain security auditing teams is still based on the more traditional form of auditing, and as we explained earlier in this article, formal verification yields orders of magnitude stronger security guarantees. What is encouraging to see is that some security auditing firms have started to experiment with some initial elements of formal verification, such as Manticore . We expect to see the increasing intersection between formal verification and security audit for blockchain code in the years to come.
Conclusion
With the explosive development of the blockchain market, especially the decentralized financial infrastructure, the need for the security of assets on the chain is imminent. The existing security audit services will not be able to meet the growing security requirement of financial infrastructure. Formal verification is a commonly used computer security technology in military, aerospace, and other fields that have very high system security requirements. It is very suitable for blockchain underlying protocols and financial infrastructure. Runtime Verification is a leader in formal verification technology in academic and industrial practice. We believe the team will establish new heightened industry standards in the field of blockchain security.
🌟 About Us
IOSG Ventures, founded in 2017, is a community-friendly and research-driven early-stage venture firm across China, the US, and Singapore. We focus on open finance, Web 3.0, and infrastructure for a decentralized economy. Our portfolio covers more than 60 projects, including Layer 1 (NEAR, Polkadot, Cosmos), DeFi (1inch, Synthetix, UMA). We commit ourselves to working alongside various developer & DAO communities and helping the most aspiring founding teams to achieve success. As a developer-friendly fund with long-term values, we launch the Kickstarter Program which offers capital and resources for innovative and courageous developers. Since we consistently cooperate with our partners and connect with communities, we work closely with our portfolio projects throughout their journey of entrepreneurship.
🌟 Join Us
Website/Kickstarter/Twitter/Linkedin/GitHub
