Here at Runtime Verification, we are spending time developing and improving tools for the K Framework. In particular, one of the projects I have been working on is a new execution engine for concrete execution of programs in K semantics, which compiles to LLVM.
Because we compile to LLVM, we are able to make use of code in any programming language that targets LLVM. In particular, we use Rust for the portion of the runtime which handles operations over lists, maps, and sets.
Yesterday I discovered a very subtle bug in our Rust code which was causing our tests to fail. It was affecting the hash algorithm we use for maps and sets, which in turn caused a map lookup operation to fail even though the key it was supposed to look up was in fact in the map.
Musab A. Alturki, Brandon Moore, Karl Palmskog and Lucas Pena
Earlier this year, Runtime Verification was engaged by Algorand to verify its consensus protocol. We are happy to report that the first part of the effort, namely modeling the protocol and proving its safety theorem, has been successfully completed. Specifically, we have used a proof assistant (Coq) to systematically identify assumptions under which the protocol is mathematically guaranteed to not fork.
At Runtime Verification, we are using Haskell to develop the next generation of formal verification tools based on the K Framework. This article describes how we use algebraic data types to write expressive Haskell code.
Bool represents a single bit of information:
data Bool = False | True
The popular term “boolean blindness” refers to the information lost by functions that operate on
Bool when richer structures are available. Erasing such structure can give code a bad smell. Using more structure can produce interfaces that are easier to document, use, decompose, and generalize.
Earlier this Fall, Runtime Verification opened a subsidiary in Bucharest, Romania. The new company, Runtime Verification SRL, is located in the heart of the capital city and already staffed by seven persons. The operation’s focus will be two-fold; support the development of the new K in Haskell, and deliver smart contract verification audits for clients building products and services for the Ethereum community and beyond. The founding team consists of Traian Serbanuta (co-inventor of the K-framework), Virgil Serbanuta, Denis Bogdanas, Vladimir Ciobanu, Denisa Diaconescu, Ana Pantilie, and Andrei Vacaru.
In February of this year Runtime Verification, Inc, (RV) received the very first security grant from the Ethereum Foundation to formally model/specify and verify the Casper smart contract.
Runtime Verification, Inc. (RV) along with the Formal Systems Lab at the University of Illinois (FSL) have announced a joint initiative targeting the full formalization of the Viper smart contract programming language, using the K Framework to create a full formal definition of this research-oriented smart contract programming language. This effort is intended to yield a number of useful tools and artifacts, and to lay the foundation for the future of principled and formally rigorous smart contract development. Today, we are happy to announce the release of our first round of fully formal tools for review to the Ethereum community.
Not long ago, one of our customers came to us confused about an analysis report on a simple program their company used internally to assess knowledge of C. Among the code they sent us was something like the following three lines:
int32_t var = 0xffeeddcc;
int32_t var2 = 0x7f000000;
var2 <<= 8;
They assumed that this code should be free from defects, and thought that possibly the two defects we reported were incorrect. Let's take a look at the error reports that result when we insert these lines into a simple program and execute them:
We've all had it happen: you write some multithreaded code, but when you run it, it crashes with some kind of error every second or third or hundredth run. The traditional way of trying to debug this problem is very tedious and involves attempting to reproduce the error (difficult) and then tracing the inconsistent state backwards to find the source of the race condition (even more difficult).
Enter RV-Predict. Today I was developing code for RV-Match when I ran into an intermittently occurring NullPointerException in its parser. Instead of trying to reproduce the bug and tracking its behavior backwards, I assumed going in that it was caused by a race condition, and ran RV-Predict on the program. After it crashed, it spat out the following error report: Continue reading