SPLASH Workshop/Symposium Events 2022
2022 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Events 2022)

Title Page

Welcome from the Chairs
This volume contains the proceedings of the Eighth ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2022), held in Auckland, New Zealand, on December 7, 2022, as a satellite event of SPLASH 2022: The ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity.
The aim of this workshop is to bring together researchers and engineers who are interested in the application of formal and semi-formal methods to improve the quality of safety-critical computer systems. FTSCS strives to promote research and development of formal methods and tools for industrial applications, and is particularly interested in industrial applications of formal methods.

Cooperative Verification: Towards Reliable Safety-Critical Systems (Invited Talk)
Dirk Beyer 
(LMU Munich, Germany)
Cooperative verification is an approach in which several verifiers help each other solving the verification problem by sharing artifacts about the verification process. There are many verification tools available, but the power of combining them is not yet fully leveraged. The problem is that in order to use verifiers 'off-the-shelf', we need clear interfaces to invoke the tools and to pass information. Part of the interfacing problem is to define standard artifacts to be exchanged between verifiers. We explain a few recent approaches for cooperative combinations and also give a brief overview of CoVeriTeam, a tool for composing verification systems from existing off-the-shelf components.

@InProceedings{FTSCS22p1, author = {Dirk Beyer}, title = {Cooperative Verification: Towards Reliable Safety-Critical Systems (Invited Talk)}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {1--2}, doi = {10.1145/3563822.3572548}, year = {2022}, } Publisher's Version

Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
Jaime Arias , Kyungmin Bae , Carlos Olarte , Peter Csaba Ölveczky , Laure Petrucci , and Fredrik Rømming 
(CNRS, France; LIPN, France; Université Sorbonne Paris Nord, France; Pohang University of Science and Technology, South Korea; University of Oslo, Norway)
This paper presents a rewriting logic semantics for parametric timed automata (PTAs) and shows that symbolic reachability analysis using Maude-with-SMT is sound and complete for the PTA reachability problem. We then refine standard Maude-with-SMT reachability analysis so that the analysis terminates when the symbolic state space of the PTA is finite. We show how we can synthesize parameters with our methods, and compare their performance with Imitator, a state-of-the-art tool for PTAs. The practical contributions are two-fold: providing new analysis methods for PTAs---e.g. allowing more general state properties in queries and supporting reachability analysis combined with user-defined execution strategies---not supported by Imitator, and developing symbolic analysis methods for real-time rewrite theories.

@InProceedings{FTSCS22p3, author = {Jaime Arias and Kyungmin Bae and Carlos Olarte and Peter Csaba Ölveczky and Laure Petrucci and Fredrik Rømming}, title = {Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {3--15}, doi = {10.1145/3563822.3569923}, year = {2022}, } Publisher's Version

Q: A Sound Verification Framework for Statecharts and Their Implementations
Samuel D. Pollard , Robert C. Armstrong , John Bender , Geoffrey C. Hulette , Raheel S. Mahmood , Karla Morris , Blake C. Rawlings , and Jon M. Aytac 
(Sandia National Laboratories, USA)
We present Q Framework: a verification framework used at Sandia National Laboratories. Q is a collection of tools used to verify safety and correctness properties of high-consequence embedded systems and captures the structure and compositionality of system specifications written with state machines in order to prove system-level properties about their implementations. Q consists of two main workflows: 1) compilation of temporal properties and state machine models (such as those made with Stateflow) into SMV models and 2) generation of ACSL specifications for the C code implementation of the state machine models. These together prove a refinement relation between the state machine model and its C code implementation, with proofs of properties checked by NuSMV (for SMV models) and Frama-C (for ACSL specifications).

@InProceedings{FTSCS22p16, author = {Samuel D. Pollard and Robert C. Armstrong and John Bender and Geoffrey C. Hulette and Raheel S. Mahmood and Karla Morris and Blake C. Rawlings and Jon M. Aytac}, title = {Q: A Sound Verification Framework for Statecharts and Their Implementations}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {16--26}, doi = {10.1145/3563822.3568014}, year = {2022}, } Publisher's Version Info

strategFTO: Untimed Control for Timed Opacity
Étienne André , Shapagat Bolat , Engel Lefaucheux , and Dylan Marinho 
(Université Sorbonne Paris Nord, France; LIPN, France; CNRS, France; Université de Lorraine, France; Inria, France; LORIA, France)
We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the total execution time. The system, here modelled by timed automata, is deemed opaque if for any execution time, there are either no corresponding runs, or both public and private corresponding runs. We focus on the untimed control problem: exhibiting a controller, ie a set of allowed actions, such that the system restricted to those actions is fully timed-opaque. We first show that this problem is not more complex than the full timed opacity problem, and then we propose an algorithm, implemented and evaluated in practice.

@InProceedings{FTSCS22p27, author = {Étienne André and Shapagat Bolat and Engel Lefaucheux and Dylan Marinho}, title = {strategFTO: Untimed Control for Timed Opacity}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {27--33}, doi = {10.1145/3563822.3568013}, year = {2022}, } Publisher's Version Info

Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic Search
Byeongjee Kang  and Kyungmin Bae 
(POSTECH, South Korea)
A concurrent system specified as a rewrite theory can be symbolically analyzed using narrowing-based reachability analysis. Narrowing-based approaches have been applied to formally analyze cryptographic protocols and parameterized protocols. However, existing narrowing-based techniques, based on a breadth-first-search strategy, cannot deal with generic distributed systems with objects and messages due to the symbolic state-space explosion problem. This paper proposes a heuristic search approach for narrowing-based reachability analysis to guide the search for counterexamples involving a small number of objects. As a result, our method can effectively find a counterexample if an error state is reachable. We demonstrate the effectiveness of our technique using a nontrivial distributed consensus algorithm.

@InProceedings{FTSCS22p34, author = {Byeongjee Kang and Kyungmin Bae}, title = {Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic Search}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {34--44}, doi = {10.1145/3563822.3568017}, year = {2022}, } Publisher's Version Info

Proving Memory Access Violations in Isabelle/HOL
Sharar Ahmadi , Brijesh Dongol , and Matt Griffin 
(University of Surrey, UK)
Security-critical applications often rely on memory isolation mechanisms to ensure integrity of critical data (e.g., keys) and program instructions (e.g., implementing an attestation protocol). These include software-based security microvisor (SµV) or hardware-based (e.g., TrustLite or SMART). Here, we must guarantee that none of the assembly-level instructions corresponding to a program violate the imposed memory access restrictions. We demonstrate our approach on two architectures (SµV and TrustLite) on which remote attestation protocols are implemented. We extend an approach based on the Binary Analysis Platform (BAP) to generate compiled assembly for a given C program, which is translated to an assembly intermediate language (BIL) and ultimately to Isabelle/HOL theories. In our extension, we develop an adversary model and define conformance predicates imposed by an architecture. We generate a set of programs covering all possible cases in which an assembly-level instruction attempts to violate at least one of the conformance predicates. This shows that the memory access restriction of both SµV and TrustLite are dynamically maintained. Moreover, we introduce conformance predicates for assembly-level instructions that can change the control flow, which improve TrustLite’s memory protection unit.

@InProceedings{FTSCS22p45, author = {Sharar Ahmadi and Brijesh Dongol and Matt Griffin}, title = {Proving Memory Access Violations in Isabelle/HOL}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {45--55}, doi = {10.1145/3563822.3568010}, year = {2022}, } Publisher's Version Published Artifact Artifacts Available

Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT
Jaeseo Lee , Sangki Kim , and Kyungmin Bae 
(POSTECH, South Korea)
A programmable logic controller (PLC) is widely used in industrial control systems, and Structured text (ST) is an imperative language to develop PLC programs. Because of its safety-critical nature, formally analyzing PLC programs is important, and a rewriting-based formal semantics of ST has been proposed for this purpose. This paper presents a bounded model checking technique for PLC ST programs based on the rewriting-based semantics. We apply rewriting modulo SMT to symbolically analyze LTL properties of ST programs with respect to sequences of (possibly infinite) inputs and outputs. We have demonstrated the effectiveness of our approach using a traffic light case study.

@InProceedings{FTSCS22p56, author = {Jaeseo Lee and Sangki Kim and Kyungmin Bae}, title = {Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {56--67}, doi = {10.1145/3563822.3568016}, year = {2022}, } Publisher's Version Info

Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation
Jiawei Chen , José Luiz Vargas de Mendonça , Shayan Jalili , Bereket Ayele , Bereket Ngussie Bekele , Zhemin Qu , Pranjal Sharma , Tigist Shiferaw , Yicheng Zhang , and Jean-Baptiste Jeannin 
(University of Michigan at Ann Arbor, USA; Addis Ababa Institute of Technology, Ethiopia)
Robots and other cyber-physical systems are held to high standards of safety and reliability, and thus one must be confident in the correctness of their software. Formal verification can provide such confidence, but programming languages that lend themselves well to verification often do not produce executable code, and languages that are executable do not typically have precise enough formal semantics. We present MARVeLus, a stream-based approach to combining verification and execution in a synchronous programming language that allows formal guarantees to be made about implementation-level source code. We then demonstrate the end-to-end process of developing a safe robotics application, from modeling and verification to implementation and execution.

@InProceedings{FTSCS22p68, author = {Jiawei Chen and José Luiz Vargas de Mendonça and Shayan Jalili and Bereket Ayele and Bereket Ngussie Bekele and Zhemin Qu and Pranjal Sharma and Tigist Shiferaw and Yicheng Zhang and Jean-Baptiste Jeannin}, title = {Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {68--79}, doi = {10.1145/3563822.3568015}, year = {2022}, } Publisher's Version

Formal Probabilistic Risk Assessment of a Nuclear Power Plant
Mohamed Abdelghany  and Sofiène Tahar 
(Concordia University, Canada)
Functional Block Diagrams (FBD) are commonly used as a graphical representation for probabilistic risk assessment in a wide range of complex engineering applications. An FBD models the stochastic behavior and cascading dependencies of system components or subsystems. Within FBD-based safety analysis, Event Trees (ET) dependability modeling techniques are typically used to associate all possible risk events to each subsystem. In this paper, we conduct the formal modeling and probabilistic risk assessment of a nuclear power plant in the HOL4 theorem prover. Using an FBD modeling in HOL4 of the nuclear Boiling Water Reactor (BWR), we formally determine all possible classes of accident events that can occur in the BWR. We compare our formal analysis in HOL4 with those obtained analytically and by simulation using Matlab and the specialized Isograph tool. Experimental results showed the superiority of our approach in terms of scalability, expressiveness, accuracy and CPU time.

@InProceedings{FTSCS22p80, author = {Mohamed Abdelghany and Sofiène Tahar}, title = {Formal Probabilistic Risk Assessment of a Nuclear Power Plant}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {80--87}, doi = {10.1145/3563822.3568018}, year = {2022}, } Publisher's Version

Modelling a Blockchain for Smart Contract Verification using DeepSEA
Daniel Britten  and Steve Reeves 
(University of Waikato, New Zealand)
To create trustworthy programs, the 'gold standard' is specifications at a high-enough level to clearly correspond to the informal specifications, and also a refinement proof linking these high-level specifications down to, in our case, executable bytecode. The DeepSEA system demonstrates how this can be done, in the context of smart contracts on the Ethereum blockchain. A key component of this is the model of the blockchain on which the smart contracts reside. When doing proofs in DeepSEA, it is critical to have such a model, which allows for the writing of specifications at a high-level clearly corresponding to informal specifications. A candidate model for doing so and its usefulness for carrying out proofs is discussed in this paper.

@InProceedings{FTSCS22p88, author = {Daniel Britten and Steve Reeves}, title = {Modelling a Blockchain for Smart Contract Verification using DeepSEA}, booktitle = {Proc.\ FTSCS}, publisher = {ACM}, pages = {88--94}, doi = {10.1145/3563822.3568011}, year = {2022}, } Publisher's Version Info