Runtime Verification seeking experienced C and C++ engineers

Runtime Verification, Inc., (RV) wants to add a Senior Software Engineer to its team that makes verification tools for C and C++ programs.

RV is a growing startup whose software tools help developers make safe, reliable software that runs on automobiles, airplanes, spacecraft, and the blockchain. RV’s verification technology is state-of-the-art, and the company employs leading experts in software engineering and verification.

RV offers great benefits, and its offices have the best views in downtown Urbana.

In the role of Senior Software Engineer, prior experience writing, testing, and debugging multithreaded C or C++ programs is essential. Familiarity with assembly language, operating system internals, embedded systems, or real-time operating systems is highly desirable.

Experience with test-driven development, Java, compiler implementation (especially using LLVM), functional programming, or formal methods is a plus.

In addition to being technically astute, a successful Senior Software Engineer at RV has to be a considerate teammate with good communication skills, and an eager learner with a demonstrable ability to solve problems.

To apply to this position, email a cover letter and résumé to contact (at) (our domain) (dot) com. Use the words “Careers” and “Senior Software Engineer” in the subject.

IELE: A New Virtual Machine for the Blockchain

IELE and K Team
Runtime Verification (RV) is proud to release their first version of IELE, a new virtual machine for the blockchain.

IELE Team Photo, left to right: Daejun Park (PhD student at UIUC, RV intern); Theodoros Kasampalis (PhD student at UIUC, RV intern); Yi Zhang (PhD student at UIUC, RV intern); Traian Serbanuta (RV; screen, left bottom); Grigore Rosu (RV president/CEO and UIUC professor; screen, center, taking the picture); Virgil Serbanuta (RV; screen, right bottom); David Young (RV); Brandon Moore (RV); Yiyi Wang (RV); Dwight Guth (RV).

Continue reading

RV Inc. & FSL @ UIUC Release First Formal Viper Tools

Taming the Viper

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.

Continue reading

ERC20-K: Formal Executable Specification of ERC20

ERC20
The ERC20 standard is one of the most important standards for the implementation of tokens within Ethereum smart contracts. ERC20 provides basic functionality to transfer tokens and to be approved so they can be spent by another on-chain third party. Unfortunately, ERC20 leaves several corner cases unspecified, which makes it less than ideal to use in the formal verification of token implementations. Indeed, we at RV, Inc., have been asked to verify smart contracts for ERC20 compliance. However, we found that it is unclear what ERC20 compliance means, because the existing presentations of ERC20 are far from serving as mathematical models of the standard token. Consequently, we decided to create ERC20-K, a mathematically rigorous formalization of ERC20, making sure that all corner cases are thought through, explicitly covered, and thoroughly tested. From here on, when we claim that we prove implementations of ERC20 tokens correct, we mean that they provably satisfy the 13 rules of ERC20-K.

Continue reading

New Technologies for the Blockchain: IELE (virtual machine) and K (universal language framework)

IELE and K Team Runtime Verification has been recently awarded a research and development contract by IOHK to design a next generation virtual machine and a universal language framework to be used as core infrastructure for future blockchain technologies. The formal analysis and verification technology employed in this project has been developed and improved over more than 15 years of research and development, both in the Formal System Laboratory (FSL) at the University of Illinois at Urbana-Champaign and at Runtime Verification, with generous funding from organisations including NSF, NASA, DARPA, NSA, Boeing, Microsoft, Toyota, and Denso. It is about time that aircraft grade, software analysis technology used for mission critical software gets deployed to smart contracts, the blockchain and cryptocurrencies. The project will be executed by a team of Runtime Verification experts led by Prof. Rosu, who will work closely with students at the University of Illinois, also funded by IOHK, and with IOHK R&D personnel. IELE and K Team Photo, left to right: Daejun Park (PhD student at UIUC, RV intern); Theodoros Kasampalis (PhD student at UIUC, RV intern); Yi Zhang (PhD student at UIUC, RV intern); Traian Serbanuta (RV; screen, left bottom); Grigore Rosu (RV and UIUC; screen, center, taking the picture); Virgil Serbanuta (RV; screen, right bottom); David Young (RV); Brandon Moore (RV); Yiyi Wang (RV); Dwight Guth (RV). Also Chris Hathhorn (RV), who missed picture.

Continue reading

RV Inc. & FSL @ UIUC to Formalize Ethereum’s Viper

Runtime Verification, Inc. (RV) along with the Formal Systems Lab at the University of Illinois (FSL) are announcing 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. We believe this effort will yield a number of useful tools and artifacts, and can lay the foundation for the future of principled and formally rigorous smart contract development.

Continue reading

RV-Match now supports inline assembly

RV-Match now supports execution of applications containing x86_64 inline assembly. If you have a program that contains inline assembly, you can compile it with kcc like any other C program and we will compile the functions containing inline assembly with gcc and execute them directly the same way we handle any other native code which we do not have C source for. As a result of this, the ability to detect undefined behavior in that function is eliminated, but it allows you to analyze complex applications which contain some code in inline assembly which you do not want to translate into C source.

Continue reading

K Framework Seeking Professional Developers

5104335The K Framework provides extensive support for writing and validating formal semantics of programming languages, and using these semantics to execute, analyze, and even verify programs. We are part of a new joint effort to advance the implementation of the K framework - and we are now hiring for this project. The organizations involved are

Positions for professional developers are available at RV, IOHK, and ADSC. The K website has full details on the projects and the available positions.

Let’s Make the Ethereum Virtual Machine Better

EVM
Ethereum Virtual Machine

The Ethereum Virtual Machine (EVM) has been recently given a complete formal semantics using the K framework, as part of the open source KEVM project.  The effort is described in detail in the KEVM technical report.  The aim of the KEVM project is to develop a suite of formal analysis tools for smart contracts based on the formal semantics of the EVM.  In other words, the only trust base for these tools will be the public EVM semantics, which is the best we can hope for.  The KEVM team currently consists of researchers and developers at Runtime Verification and in the Formal Systems Laboratory at the University of Illinois, and the project is being partially funded by IOHK.

K
K Framework

While defining the formal semantics of EVM in K, there were moments when we asked ourselves "Why did they do it this way?"  Also, while verifying smart contracts using the semantics, we found some of the design choices made by the EVM designers questionable; if nothing else, they make verification harder.  We have decided to then collect our thoughts during the semantic definition process and during verification of smart contracts after.  They were bundled together with the KEVM definition, under issues.md.  Here we restate them so you can find them all in one place in order to express your thoughts.  Maybe it is not too late to re-design the EVM, this time with formal semantics and mathematical rigor in mind.  If the blockchain technology is here is stay, then we should better build it on the most solid foundation that we can.

 

Continue reading

Undefined Behavior Review: tis-interpreter vs. RV-Match

John Regher's blog is a great source for anyone concerned about undefined behavior in C programs. The latest installment Undefined Behavior in 2017, written jointly with Pascal Cuoq, reviews the state of popular tools for detecting important categories of undefined behavior, and describes a new tool tis-interpreter that they have been working with.

At Runtime Verification we are big proponents of dynamic program analysis and rigorous error detection, so we were excited to hear of another tool following a similar approach to our own undefined-behavior checker, RV-Match(which is the commercial continuation of the academic kcc tool). We tested the most recent available version of tis-interpreter against RV-Match. With roots in the Frama-C verification project, we would hope tis-interpreter is faithful to the C standard - or become concerned that Frama-C could "prove" wrong code correct. We found that tis-interpreter detects many fewer errors than RV-Match, and has missing or incorrect implementations of several language features and almost all library functions. On the positive side, their examples revealed a few errors in RV-Match, which we have now fixed. We will update this post for improvements in tis-interpreter.

Continue reading