Two tutorials that are related to the theme of PRDC conference series.

Tutorial 1    The K Framework: A tool kit for language semantics and verification

Abstract

The K Framework (https://kframework.org/) provides a set of tools for developing programming languages and formal analysis tools. By writing a single description of your language’s syntax and operational semantics, you can use K to automatically extract a parser, interpreter, symbolic execution engine, and many more tools for your language. This approach scales well: K implementations have been built for many mainstream programming languages (C, Rust, Java, Python, EVM, to name a few), and K is used in practice every day for real verification problems.

This tutorial is aimed at anyone who is interested in programming language implementation or program verification, and will be broken down into two main sessions (AM and PM session):

AM session: We will build a simple imperative language in K, where we will define syntax and operational semantics of the language we are building. With the language definition in hand, we will take advantage of K’s support for deductive verification to write some simple proofs over programs. By the end of this session, the attendees should be able to implement and verify their next research DSL or language of interest using K.

PM session: We will verify the properties of Ethereum smart contracts using KEVM, a complete formal semantics of Ethereum Virtual Machine (EVM). To provide the attendees with the necessary background knowledge, we will go through the basics of blockchain, EVM, Solidity—the most popular smart contract language, and Foundry—a reliable and easy-to-setup tool that is widely used by smart contract developers and auditors, before moving onto KEVM. By the end of this session, the attendees will be able to prove properties of Ethereum smart contracts by defining them through test functions in Foundry and verifying them using KEVM.

NOTE TO ATTENDEE

If you want to join the hands-on sessions, please install K and KEVM prior to the tutorial as it may take 30min to 1 hour to install. This can be done using the K Framework installer `kup`, with the instructions available in its repository: https://github.com/runtimeverification/kup.

SPEAKER

Jin Xing Lim is a formal verification engineer at Runtime Verification Inc, where he develops software tools to detect security issues on smart contracts, particularly in the Ethereum ecosystem. Previously, he received his B.Sc. in Mathematics (2014) from the National University of Singapore and Ph.D. in Engineering Systems and Design (2022) from the Singapore University of Technology and Design, where he worked on interactive theorem provers and blockchain applications. Prior to his Ph.D., he also worked as a lecturer (2014 – 2018) at Temasek Polytechnic, where he taught subjects related to mathematics and statistics.

Palina Tolmach is a formal verification engineer and researcher with a focus on formal analysis of smart contracts. Prior to joining RV, Palina received her PhD from Nanyang Technology University in Singapore, where she researched and developed tools for smart contract verification and automated repair. She also worked on bridging the gap between theory and practice of verification with major organizations in crypto. She is broadly interested in formal methods, software engineering and program synthesis. Palina strongly believes that formal verification can and should be part of the software development lifecycle.

Tutorial 2   Developing Assurance Cases with AdvoCATE

Abstract

Safety/assurance cases represent the state of the art in assurance technologies, and are often required for applications in many safety-critical domains (e.g., nuclear, automotive, railroad, defense, medical devices, etc.). They are also applicable in domains where regulations have not yet kept up with technology, such as autonomous vehicles.

An assurance case demonstrates that the risks associated with a specific system concern (such as safety, security, etc.) have been identified, are well-understood, have been appropriately controlled, and that there are processes in place to monitor the performance and effectiveness of the risk management measures. Thus, assurance cases are risk management artifacts whose purpose is to convince the various stakeholders of a system, that the system has been designed to be safe, is operated safely, and that it meets the required assurance properties.

AdvoCATE implements an integrated assurance model that combines hazard analysis, requirements, structured arguments, barrier models (bow tie diagrams), and verification artifacts.

This tutorial will give hands-on experience using the NASA-developed AdvoCATE toolset for creating safety/assurance cases.

SPEAKER

Dr. Ewen Denney is a senior computer scientist with KBR, KBR Technical Fellow, and the Technical Area Liaison for the Robust Software Engineering group at the NASA Ames Research Center in California.

He currently leads a research group that is seeking to establish a rigorous basis for safety cases, in particular software safety cases, develop tool support, and apply this work to problems in a variety of industries. He has worked on automated code generation, formal certification, and safety analysis in the aerospace domain, developing AI-based systems for the automated generation of code for scientific computation, and the certification of autocode.

Most recently, he has developed the AdvoCATE assurance case automation toolset, as product manager and technical lead, and with his colleagues, submitted the first ever UAS civilian safety case that has been accepted by the FAA.