Related papers: A Proof-Producing Compiler for Blockchain Applicat…
Cryptographic interactive proof systems provide an efficient and scalable means of verifying the results of computation on blockchain. A prover constructs a proof, off-chain, that the execution of a program on a given input terminates with…
Most software domains rely on compilers to translate high-level code to multiple different machine languages, with performance not too much worse than what developers would have the patience to write directly in assembly language. However,…
This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for…
Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing…
This demo abstract introduces a new light-weight programming language koa which is suitable for blockchain system design and implementation. In this abstract, the basic features of koa are introduced including working system (with…
For all the successes in verifying low-level, efficient, security-critical code, little has been said or studied about the structure, architecture and engineering of such large-scale proof developments. We present the design, implementation…
Simplicity is a typed, combinator-based, functional language without loops and recursion, designed to be used for crypto-currencies and blockchain applications. It aims to improve upon existing crypto-currency languages, such as Bitcoin…
In recent years, many decentralized applications based on blockchain (DApp) have been developed. However, due to inadequate testing, DApps are easily exposed to serious vulnerabilities. We find three main challenges for DApp testing, i.e.,…
Blockchain technology promises a decentralized, trustless, and interoperable infrastructure. However, widespread adoption remains hindered by issues such as limited scalability, high transaction costs, and the complexity of maintaining…
A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a typing error or bad memory management. However, errors can become a significant issue if the unsafe…
Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control assets, which are often of high…
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive…
Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a…
Caesar is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative intermediate verification language based on the real-valued logic HeyLo. HeyVL allows users to express a probabilistic program, its…
Developing secure distributed systems is difficult, and even harder when advanced cryptography must be used to achieve security goals. Following prior work, we advocate using secure program partitioning to synthesize cryptographic…
OCaml is particularly well-fitted for formal verification. On one hand, it is a multi-paradigm language with a well-defined semantics, allowing one to write clean, concise, type-safe, and efficient code. On the other hand, it is a language…
Verifying the execution of a program is complicated and often limited by the inability to validate the code's correctness. It is a crucial aspect of scientific research, where it is needed to ensure the reproducibility and validity of…
Foundational verification allows programmers to build software which has been empirically shown to have high levels of assurance in a variety of important domains. However, the cost of producing foundationally verified software remains…
In this paper, we present the first intrinsically secure and semantically universal omnichain interoperability protocol: LayerZero. Utilizing an immutable endpoint, append-only verification modules, and fully-configurable verification…
The Blockchain and the programs running on it, called Smart Contracts, are more and more applied in all fields requiring trust and strong certifications. In this work we compare public and permissioned blockchains for industrial…