Verifying the functional correctness of a circuit is often the most time-consuming part of the design process. Recently, world-level formal verification methods, e.g., Binary Moment Diagram (BMD) and Symbolic Computer Algebra (SCA) have reported very good results for proving the correctness of arithmetic circuits. However, these techniques still frequently fail due to memory or time requirements. The unknown complexity bounds of these techniques make it impossible to predict before invoking the verification tool whether it will successfully terminate or run for an indefinite amount of time.

In this paper, we formally prove that for integer arithmetic circuits, the entire verification process requires at most linear space and quadratic time with respect to the size of the circuit function. This is shown for the two main word-level verification methods: backward construction using BMD and backward substitution using SCA. We support the architectures which are used in the implementation of integer polynomial operations, e.g., X³ - XY² + XY. Finally, we show in practice that the required space and run times of the word-level methods match the predicted results in theory when it comes to the verification of different arithmetic circuits, including exponentiation circuits with different power values (X^P : 2 ≤ P ≤ 7) and more complicated circuits (e.g., X² + XY + X).

Software model checking has recently started to be applied in the verification of programmable logic controller (PLC) programs. It works efficiently when the number of input variables is limited, their interaction is small and, thus, the number of states the program can reach is not large. As observed in the large code base of the CERN industrial PLC applications, this is usually not the case: it thus leads to the well-known state-space explosion problem, making it impossible to perform model checking. One of the main reasons that causes state-space explosion is the inclusion of numeric variables due to the wide range of values they can take. In this paper, we propose an approach to discretize PLC input numeric variables (modelled as non-deterministic). This discretization is complemented with a set of transformations on the control-flow automaton that models the PLC program so that no extra behaviours are added. This approach is then quantitatively evaluated with a set of empirical tests using the PLC model checking framework PLCverif and three different state-of-the-art model checkers (CBMC, nuXmv, and Theta), showing beneficial results for BDD-based model checkers.

Many embedded system applications impose hard real-time, energy or safety requirements on corresponding programs typically concurrently executed on a given MPSoC target platform. Even when mutually isolating applications in space or time, the enforcement of such properties, e.g., by adjusting the number of processors allocated to a program or by scaling the voltage/frequency mode of involved processors, is a difficult problem to solve, particularly in view of typically largely varying environmental input (workload) per execution. In this paper, we formalize the related control problem using finite state machine models for the uncertain environment determining the workload, the system response (feedback), as well as the enforcer strategy. The contributions of this paper are as follows: a) Rather than trace-based simulation, the uncertain environment is modeled by a discrete-time Markov chain (DTMC) as a random process to characterize possible input sequences an application may experience. b) A number of important verification goals to analyze different enforcer FSMs are formulated in PCTL for the resulting stochastic verification problem, i.e., the likelihood of violating a timing or energy constraint, or the expected number of steps for a system to return to a given execution time corridor. c) Applying stochastic model checking, i.e., PRISM to analyze and compare enforcer FSMs in these properties, and finally d) proposing an approach for reducing the environment DTMC by partitioning equivalent environmental states (i.e., input states leading to an equal system response in each MPSoC mode) such that verification times can be reduced by orders of magnitude to just a few ms for real-world examples.

The performance of many accelerator architectures depends on the communication with external memory. During execution, new I/O data is continuously fetched forth and back to memory. This data exchange is very often performance-critical and a careful orchestration thus vital. To satisfy the I/O demand for accelerators of loop nests, it was shown that the individual reads and writes can be merged into larger blocks, which are subsequently transferred by a single DMA transfer. Furthermore, the order in which such DMA transfers must be issued, was shown to be reducible to a real-time task scheduling problem to be solved at run time. Rather than just concepts, we investigate in this paper efficient algorithms, data structures and their implementation in hardware of such a programmable Loop I/O Controller architecture called LION that only needs to be synthesized once for each processor array size and I/O buffer configuration, thus supporting a large class of processor arrays. Based on a proposed heap-based priority queue, LION is able to issue every 6 cycles a new DMA request to a memory bus. Even on a simple FPGA prototype running at just 200 MHz, this allows for more than 33 million DMA requests to be issued per second. Since the execution time of a typical DMA request is in general at least one order of magnitude longer, we can conclude that this rate is sufficient to fully utilize a given memory interface. Finally, we present implementations on FPGA and also 22nm FDX ASIC showing that the overall overhead of a LION typically amounts to less than 5% of an overall processor array design.

We apply reinforcement learning to approximate the optimal probability that a stochastic hybrid system satisfies a temporal logic formula. We consider systems with (non)linear continuous dynamics, random events following general continuous probability distributions, and discrete nondeterministic choices. We present a discretized view of states to the learner, but simulate the continuous system. Once we have learned a near-optimal scheduler resolving the choices, we use statistical model checking to estimate its probability of satisfying the formula. We implemented the approach using Q-learning in the tools HYPEG and modes, which support Petri net- and hybrid automata-based models, respectively. Via two case studies, we show the feasibility of the approach, and compare its performance and effectiveness to existing analytical techniques for a linear model. We find that our new approach quickly finds near-optimal prophetic as well as non-prophetic schedulers, which maximize or minimize the probability that a specific signal temporal logic property is satisfied.

Wearable and implantable medical devices are being increasingly deployed for diagnosis, monitoring, and to provide therapy for critical medical conditions. Such medical devices are examples of safety-critical, cyber-physical systems. In this paper we focus on insulin infusion systems (IISs), which are used by diabetics to maintain safe blood glucose levels. These systems support wireless features introducing potential vulnerabilities. Although these devices go through rigorous safety certification processes, these are not able to mitigate security threats. Based on published literature, attackers can remotely command to inject an incorrect amount of insulin thereby posing threat to a patient's life. While prior work based on formal methods have been proposed to detect potential attack vectors using different forms of static analysis, these have limitations in preventing attacks at run-time. Also, as these devices are safety critical, it is not possible to apply security patches, when new types of attacks are detected, due to the need for recertification.

This paper addresses these limitations by developing a formal framework for the detection of cyber-physical attacks on an IIS. First, we propose a wearable device that senses the familiar ECG to detect attacks. Thus, this device is separate from the insulin infusion system, ensuring no need for recertification of IISs. To facilitate the design of this device, we establish a correlation of ECG intervals and blood glucose levels using statistical analysis. This helps us in proposing a framework for security policy mining using the developed statistical analysis. This paves the way for the design of formal verification monitors for IISs for the first time. We perform performance evaluation of the verification monitor, which proves the technical feasibility for the design of wearable devices for attack detection of IISs. Our approach is amenable to the application of security patches, when new attack vectors are detected, making the approach ideal for run-time monitoring of medical CPSs.

In this paper, a translation from structured sequential programs to equivalent dataflow process networks (DPNs) is presented that is based on a carefully chosen set of nodes including load/store operations to access a shared global memory. For every data structure stored in the main memory, we use corresponding tokens to enforce the sequential ordering of load/store operations accessing that data structure as far as needed. Except for the load/store nodes, all nodes obey the Kahn principle so that they are deterministic in the sense that the same inputs are always mapped to the same outputs regardless of the execution schedule of the nodes. Due to the sequential ordering of load/store nodes, determinacy is also maintained by them. Moreover, the generated DPNs are quasi-static, i.e., they have schedules that are bounded in a very strict sense: For every statement of the sequential program, the corresponding DPN behaves like a homogeneous synchronous actor, i.e., it consumes one value of each input port and will finally provide one value on each output port. Hence, no more than one value needs to be stored in each buffer.

From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires reasoning about complex spatio-temporal properties of physical and computational entities that are dynamically interconnected and arranged in a particular spatial configuration. Spatio-Temporal Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and reason about spatio-temporal properties. STREL considers each system's entity as a node of a dynamic weighted graph representing its spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterizing the node's behavior. While there are offline algorithms available for monitoring STREL specifications over logged simulation traces, here we investigate for the first time an online algorithm enabling the runtime verification during the system's execution or simulation. Our approach extends the original framework by considering imprecise signals and by enhancing the logics' semantics with the possibility to express partial guarantees about the conformance of the system's behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.

The fault of one device on a grid may incur severe economical or physical damages. Among the many critical components in such IoT devices, the operating system's bootloader comes first to initiate the trusted function of the device on the network. However, a bootloader uses hardware-dependent features that make its functional correctness proof difficult. This paper uses verified programming to automate the verification of both the C libraries and assembly boot-sequence of such a, real-world, bootloader in an operating system for ARM-based IoT devices: RIoT. We first define the ARM ISA specification, semantics and properties in F* to model its critical assembly code boot sequence. We then use Low*, a DSL rendering a C-like memory model in F*, to implement the complete bootloader library and verify its functional correctness and memory safety. Other than fixing potential faults and vulnerabilities in the source C and ASM bootloader, our evaluation provides an optimized and formally documented code structure, a reasonable specification/implementation ratio, a high degree of proof automation and an equally efficient generated code.

Cyber-physical systems are notoriously hard to verify due to the complex interaction between continuous physical behavior and discrete control. A widespread and important class is formed by digital controllers that operate on fixed control cycles to interact with the physical environment they are embedded in. This paper presents a case study for integrating such controllers into a rigorous verification method for cyber-physical systems, using flowpipe-based verification methods to verify legally binding requirements for electrified vehicles to a custom bike design. The controller is integrated in the underlying model in a way that correctly represents the input discretization performed by any digital controller.

Programmable logic controllers operating in a sequential execution scheme are widely used for various applications in industrial environments with real-time requirements. The graphical programming languages described in the third part of IEC 61131 are often intended to perform open and closed loop control tasks. Continuous Function Charts (CFCs) represent an additional language accepted in practice which can be interpreted as an extension of IEC 61131-3 Function Block Diagrams. Those charts allow more flexible positioning and interconnection of function blocks, but can quickly become difficult to manage. Furthermore, the sequential execution order forces a sequential processing of possible independent and thus possibly parallel program paths. The question arises whether a translation of existing CFCs to synchronous programs considering independent actions can lead to a more manageable software model. While current formalization approaches for CFCs primarily focus on verification, the focus of this approach is on restructuring and possible reuse in engineering. This paper introduces a possible automated translation of CFCs to imperative synchronous Quartz programs and outlines the potential for reducing the states of equivalent extended finite state machines through restructuring.

We present the design and formal analysis of a remote attestation protocol and accompanying security architecture that generate evidence of trustworthy execution for legacy software. For formal guarantees of measurement ordering and cryptographic evidence strength, we leverage the Copland language and Copland Virtual Machine execution semantics. For isolation of attestation mechanisms we design a layered attestation architecture that leverages the seL4 microkernel. The formal properties of the protocol and architecture together serve to discharge assumptions made by an existing higher-level model-finding tool to characterize all ways an active adversary can corrupt a target and go undetected. As a proof of concept, we instantiate this analysis framework with a specific Copland protocol and security architecture to measure a legacy flight planning application. By leveraging components that are amenable to formal analysis, we demonstrate a principled way to design an attestation protocol and argue for its end-to-end correctness.

In this paper we present ShapEx, a tool that generates random behaviors from shape expressions, a formal specification language for describing sophisticated temporal behaviors of CPS. The tool samples a random behavior in two steps: (1) it first explores the space of qualitative parameterized shapes and then (2) instantiates parameters by sampling a possibly non-linear constraint. We implement several sampling strategies in the tool that we present in the paper and demonstrate its applicability on two use scenarios.

As the number of Internet of Things (IoT) devices proliferate, an in-depth understanding of the IoT attack surface has become quintessential for dealing with the security and reliability risks. IoT devices and components execute implementations of various communication protocols. Vulnerabilities in the protocol stack implementations form an important part of the IoT attack surface. Therefore, finding memory errors in such implementations is essential for improving the IoT security and reliability. This paper presents a tool, SEESAW, that is built on top of a static analysis tool and a symbolic execution engine to achieve scalable analysis of protocol stack implementations. SEESAW leverages the API model of the analyzed code base to perform component-level analysis. SEESAW has been applied to the USB and Bluetooth modules within the Linux kernel. SEESAW can reproduce known memory vulnerabilities in a more scalable way compared to baseline symbolic execution.

IEEE 1588 is a time synchronization protocol that is extensively used by many Cyber-Physical Systems (CPSs). However, this protocol is prone to various types of attacks. We focus on a specific type of Man-in-the-Middle (MITM) attack, where the attacker introduces random delays to the messages being exchanged between a master and a slave. Such attacks have been modelled previously and some mitigation strategies have also been developed. However, the proposed methods work only under constant delay attacks and the developed mitigation strategies are ad-hoc. We propose the first formal framework for modelling and mitigating time delay attacks in IEEE 1588. Initially, the master, the slave and the communication medium are modelled as Timed Automata (TA) assuming the absence of any attacks. Subsequently, a generic attacker is modelled as a TA, which can formally represent various attacks including constant delay, linear delay and exponential delay. Finally, system identification methods of control theory is used to design proportional controllers for mitigating the effects of time delay attacks. We use model checking to ensure the resilience of protocol to time delay attacks using the proposed mitigation strategy.