CHESS Industrial Day 2023

The aim of CHESS Industrial Day 2023 is to bring together researchers and practitioners in formal methods from industry and academia. The event provides an informal platform for exchanging practical experience with methods and tools for software analysis/verification/testing, and discussing their benefits and bottlenecks. It is organized by the Cyber-security Excellence Hub in Estonia and South Moravia (CHESS).

Date: December 8, 2023
Place: KYPO, Faculty of Informatics, Masaryk University, Botanická 68a, 60200 Brno, CZ
Contact: Antonín Kučera (FI MUNI), Jan Strejček (FI MUNI), Tomáš Vojnar (FIT BUT)

The Program includes invited presentations reporting the use/advantages/bottlenecks of formal methods in industrial practice and tool demos. Coffee, light snacks, and lunch are provided by the organizers, and there is enough space for informal communication.

8:40 - 9:00	Registration
9:00 - 9:10	Opening
9:10 - 10:30	Talks I Martin Hruška (Certora) Formal Verification of Smart Contracts Abstract: Certora develops one of the industry-leading tools for formal verification of smart contracts. In this presentation, we will provide an overview of our verification method and then focus on the application of state-of-the-art formal methods, particularly SMT solvers, within our tool. Finally, we will discuss the lessons learned from verifying the code of our clients. Viktor Malík (Red Hat) eBPF: Verification Directly in the Linux Kernel Abstract: In this talk, I will introduce eBPF, an in-kernel virtual machine for Linux that allows privileged users to execute custom programs in the kernel context. Since this introduces a number of potential problems (particularly eBPF programs crashing or stalling the kernel), each program must be verified before being loaded into the kernel. I will describe various techniques that the eBPF verifier uses as well as give an overview of some research ongoing in this area. Tomáš Kratochvíla (Honeywell) Formal Verification in Honeywell Aerospace Abstract: Although aerospace software requires extensive verification, formal methods are still rarely used, and testing is mostly done manually. Our Advanced Technology team has successfully deployed automated formal methods to detect defects in requirements and C/C++ source codes. However, our experience with verifying and analyzing machine reasoning systems for the worst-case has taught us that we must first develop an actual hard real-time memory-restricted machine reasoning system.
10:30 - 11:00	Coffee Break
11:00 - 12:00	Talks II Lukáš Zaoral and Vincent Mihalkovič (Red Hat) Static and Dynamic Analysis of a Linux Distribution Abstract: Explore the pivotal role of static and dynamic analysis in Red Hat's RPM package ecosystem. Delve into reproducible builds, upstream-downstream dynamics, and the impact of static analysis on developers. Uncover the intricacies of dynamic analysis and ELF interpreters. The presentation covers the usage of various tools like csmock, OpenScanHub, and a focus on differential analysis with ShellCheck, providing key insights into Red Hat's software distribution practices. David Kozák (Oracle Labs) Whole-Program Points-to Analysis in GraalVM Native Image Abstract: GraalVM Native Image is an ahead-of-time compiler for Java bytecode that creates standalone native executables called images. During the compilation process, a unique combination of points-to analysis, class initialization at build time, and heap snapshotting is used to optimize the application. In this talk, I will describe how points-to analysis is used inside GraalVM Native Image, the technical challenges we had to overcome to make it scalable for large real-world applications and discuss the potential of future research in this area.
12:00 - 13:00	Lunch (preceded by a group photo)
13:00 - 14:15	Tools I Ondra Vašíček and Jan Fiedor (FIT BUT / Honeywell) Unite/UniC – Making Analysis Tools More Accessible Using an OSLC-based Service-Oriented Architecture Abstract: We present a service-oriented architecture that allows developers to easily introduce new analysis tools to their users and the users to immediately be able to use these tools from their applications. The architecture consists of three main components: (1) Unite, a universal OSLC adapter able to transform any non-interactive command line tool into an OSLC-compliant web service, (2) UniC, a Java-based and Eclipse-compatible Client for Unite which can be configured for any tool transformed by Unite due to its flexible and highly extensible architecture, and (3) Eclipse Arrowhead, an IoT framework enabling automatic discovery of services provided by the analysis tools through Unite. https://pajda.fit.vutbr.cz/verifit/unite Viktor Malík (Red Hat / FIT BUT) DiffKemp – Automatically Checking Semantic Equivalence in Large-Scale C Projects Abstract: The talk will present DiffKemp – a tool for static analysis of semantic equivalence between versions of large-scale C projects. Contrary to existing tools, usually based on formal methods, DiffKemp uses a unique combination of pattern matching with lightweight static analysis and control-flow transformations. Thanks to the used approach, DiffKemp, unlike other existing tools, gives practical results on projects of the size of the Linux kernel. https://github.com/viktormalik/diffkemp Marek Trtík (FI MUNI) Fizzer Abstract: Fizzer is a new gray-box fuzzer of C programs. Its goal is to produce a test suite maximizing the branch coverage. That is achieved by a dynamic taint analysis and a gradient descent. https://github.com/staticafi/sbt-fizzer
14:15 - 14:45	Coffee Break
14:45 - 16:00	Tools II Tomáš Fiedor and Jiří Pavela (FIT BUT / Red Hat) Perun – Performance Under Control Abstract: Manual management of the performance of one's project is a tedious job. Perun is a lightweight performance version system as well as a tool suite that helps developers keep the resource consumption of their projects in check throughout the development. In this talk, we will present some of our results and recent advancements in the field of performance analysis and testing. https://github.com/Perfexionists/perun Vesal Vojdani (University of Tartu) Goblint & GobPie: Towards Usable Data Race Verification Abstract: Goblint is an automated software verifier focusing primarily on data races. Our recent focus has been on usability. I will discuss our work on interactive abstract interpretation of multi-threaded programs and demo its implementation in our IDE integration, GobPie. https://goblint.in.tum.de Martin Jonáš (FI MUNI) Symbiotic Abstract: The presentation introduces Symbiotic, a state-of-the-art program analysis tool developed at the Faculty of Informatics, Masaryk University. Symbiotic works with C programs and focuses on finding assertion violations, memory errors, memory leaks, and undefined behavior. Symbiotic can also prove that such errors are not present in the given program. https://staticafi.github.io/symbiotic
16:00	Closing

The event is funded by the European Union under the Grant Agreement No. 101087529.