Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when certifying properties of binary (machine) code in trustworthy systems, e.g., cryptographic routines. We present a theory of forward symbolic execution for unstructured programs suitable for use in theorem provers that enables automated verification of both functional and non-functional program properties. The theory’s foundation is a set of inference rules where each member corresponds to an operation in a symbolic execution engine. The rules are designed to give control over the tradeoff between the preservation of precision and introduction of overapproximation. We instantiate our theory for BIR, a previously proposed intermediate language for binary analysis. We demonstrate how symbolic executors can be constructed for BIR with common optimizations such as pruning of infeasible symbolic states. We implemented our theory in the HOL4 theorem prover using the HolBA binary analysis library, obtaining machine-checked proofs of soundness of symbolic execution for BIR. We practically evaluated two applications of our theory: verification of functional properties of RISC-V binaries and verification of execution time bounds of programs running on the ARM Cortex-M0 processor. The evaluation shows that such verification can be automated with moderate overhead on medium-sized programs.

Many types of formal verification establish properties about abstract high-level program representations, leaving a large gap to programs at runtime. Although gaps can sometimes be narrowed by techniques such as refinement, a verified program's trusted computing base may still include compilers and inlined assembly. In contrast, verification of binaries following an Instruction Set Architecture (ISA) such as RISC-V can ensure that machine code behaves as expected on real hardware. While binary analysis is useful and sometimes even necessary for ensuring trustworthiness of software systems, existing tools do not have a formal foundation or lack automation for verification. We present a workflow and toolchain based on the HOL4 theorem prover and the HolBA binary analysis library for trustworthy formal verification of RISC-V binaries. The toolchain automates proofs of binary contracts by forward symbolic execution of programs in HolBA's intermediate language, BIR. We validated our toolchain by verifying correctness of RISC-V binaries with (1) an implementation of the ChaCha20 stream cipher and (2) hand-written assembly for context switching in an operating system kernel.

Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using slh that often results in over-protection, which incurs performance overhead. We extended an existing side-channel model validation framework, Scam-V, to check the vulnerability of programs to Spectre-PHT attacks and optimize the protection of programs using the slh approach. We illustrate the efficacy of Scam-V by first demonstrating that it can automatically identify Spectre vulnerabilities in real programs, e.g., fragments of crypto-libraries. We then develop an optimization mechanism that validates the necessity of slh hardening w.r.t. the target platform. Our experiments showed that hardening introduced by LLVM in most cases could be significantly improved when the underlying microarchitecture properties are considered.

We propose a proof-producing symbolic execution for verification of machine-level programs. The analysis is based on a set of core inference rules that are designed to give control over the tradeoff between preservation of precision and the introduction of overapproximation to make the application to real world code useful and tractable. We integrate our symbolic execution in a binary analysis platform that features a low-level intermediate language enabling the application of analyses to many different processor architectures. The overall framework is implemented in the theorem prover HOL4 to be able to obtain highly trustworthy verification results. We demonstrate our approach to establish sound execution time bounds for a control loop program implemented for an ARM Cortex-M0 processor.

Observational models enable the analysis of information flow properties against side channels. Relational testing has been used to validate the soundness of these models by measuring the side channel on states that the model considers indistinguishable. However, unguided search can generate test states that are too similar to each other to invalidate the model. To address this we introduce observation refinement, a technique to guide the exploration of the state space to focus on hardware features of interest. We refine observational models to include fine-grained observations that characterize behavior that we want to exclude. States that yield equivalent refined observations are then ruled out, reducing the size of the space. We have extended an existing model validation framework, Scam-V, to support refinement. We have evaluated the usefulness of refinement for search guidance by analyzing cache coloring and speculative leakage in the ARMv8-A architecture. As a surprising result, we have exposed SiSCLoak, a new vulnerability linked to speculative execution in Cortex-A53.

Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior.

The recent Spectre attacks have demonstrated that modern microarchitectural optimizations can make software insecure. These attacks use features like pipelining, out-of-order and speculation to extract information about the memory contents of a process via side-channels. In this paper we demonstrate that Cortex-A53 is affected by speculative leakage even if the microarchitecture does not support out-of-order execution. We named this new class of vulnerabilities SiSCloak.

Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce the novel Hoare-style program logic ℒ_A , which interprets postconditions relative to program points when these are first encountered. The logic can support both partial and total correctness, derive contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of ℒ_A have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, making it applicable to the ARMv6 and ARMv8 instruction sets.

Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: the adoption of hardware-independent intermediate representations, a mechanism to translate architecture dependent code to this representation, and a set of architecture independent analyses that process the intermediate representation. The usage of these platforms to verify software introduces the need for trusting both the correctness of the translation from binary code to intermediate language (called transpilation) and the correctness of the analyses. Achieving a high degree of trust is challenging since the transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encodings (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). Similarly, analyses can use complex transformations (e.g. loop unrolling) and simplifications (e.g. partial evaluation) of the artifacts, whose bugs can jeopardize correctness of the results. We overcome these problems by developing a binary analysis platform on top of the interactive theorem prover HOL4. First, we formally model a binary intermediate language and we prove correctness of several supporting tools (i.e. a type checker). Then, we implement two proof-producing transpilers, which respectively translate ARMv8 and CortexM0 programs to the intermediate language and generate a certificate. This certificate is a HOL4 proofdemonstrating correctness of the translation. As demonstrating analysis, we implement a proof-producing weakest precondition generator, which can be used to verify that a given loop-free program fragment satisfies a contract. Finally, we use an AES encryption implementation to benchmark our platform.

In order to handle the complexity and heterogeneity of modern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representations. The usage of these platforms to verify systems down to binary-level is appealing due to the high degree of automation they provide. However, it introduces the need for trusting the correctness of the translation from binary code to intermediate language. Achieving a high degree of trust is challenging since this transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encoding (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). We overcome these problems by formally modeling one of such intermediate languages in the interactive theorem prover HOL4 and by implementing a proof-producing transpiler. This tool translates ARMv8 programs to the intermediate language and generates a HOL4 proof that demonstrates the correctness of the translation in the form of a simulation theorem. We also show how the transpiler theorems can be used to transfer properties verified on the intermediate language to the binary code.

The IEC 61499 standard provides means to specify distributed control systems in terms of function blocks. For the deployment, each device may hold one or many logical resources, each consisting of a function block network with service interface blocks at the edges. The execution model is event driven (asynchronous), where triggering events may be associated with data (and seen as messages). In this paper, we propose a low-complexity implementation technique allowing to assess end-to-end response times of event chains spanning over a set of networked devices. Based on a translation of IEC 61499 to RTFM1-tasks and resources, the response time for each task in the system at the device-level can be derived using established scheduling techniques. In this paper, we develop a holistic method to provide safe end-to-end response times taking both intra and interdevice delivery delays into account. The novelty of our approach is the accuracy of the system scheduling overhead characterization. While the device-level (RTFM) scheduling overhead was discussed in previous works, the network-level scheduling overhead for switched Ethernets is discussed in this paper. The approach is generally applicable to a wide range of commercial off-the-shelf Ethernet switches without a need for expensive custom solutions to provide hard real-time performance. A behavior characterization of the utilized switch determines the guaranteed response times. As a use case, we study the implementation onto (single-core) Advanced RISC Machine (ARM)-cortex-based devices communicating over a switched Ethernet network. For the analysis, we define a generic switch model and an experimental setup allowing us to study the impact of network topology as well as 802.1Q quality of service in a mixed critical setting. Our results indicate that safe sub millisecond end-to-end response times can be obtained using the proposed approach.

Embedded systems for critical applications are typically specified with requirements on predictable timing and safety. While ensuring predictable timing, the RTFM-lang (Real-Time For the Masses) model of computation (MoC) currently lacks memory access protection among real-time tasks. In this paper, we discuss how to safely verify task execution given a specification using the RTFM-MoC. Furthermore, an extension to the RTFM-core infrastructure is outlined and tested with use cases of embedded development. We propose a method for run time verification exploiting memory protection hardware. For this purpose, we introduce memory resources to the declarative language RTFM-core allowing compliance checks. As a proof of concept, compiler support for model analysis and automatic generation of run time verification code is implemented together with an isolation layer for the RTFM-kernel. With this verification foundation, functional run time checks as well as further overhead assessments are future research questions.

Robustness, real-time properties and resource efficiency are key properties to embedded devices of the CPS/IoT era. In this paper we propose a language approach RTFM-core, and show its potential to facilitate the development process and provide highly efficient and statically verifiable implementations. Our programming model is reactive, based on the familiar notions of concurrent tasks and (single-unit) resources. The language is kept minimalistic, capturing the static task, communication and resource structure of the system. Whereas C-source can be arbitrarily embedded in the model, and/or externally referenced, the instep to mainstream development is minimal, and a smooth transition of legacy code is possible. A prototype compiler implementation for RTFM-core is presented. The compiler generates C-code output that compiled together with the RTFM-kernel primitives runs on bare metal. The RTFM-kernel guarantees deadlock-lock free execution and efficiently exploits the underlying interrupt hardware for static priority scheduling and resource management under the Stack Resource Policy. This allows a plethora of well-known methods to static verification (response time analysis, stack memory analysis, etc.) to be readily applied. The proposed language and supporting tool-chain is demonstrated by showing the complete process from RTFM-core source code into bare metal executables for a lightweight ARM-Cortex M3 target.

The IEC 61499 standard provides means to specify distributed control systems in terms of function blocks. The execution model is event driven (asynchronous), where triggering events may be associated with data (and seen as a message). In this paper we propose a low complexity implementation technique allowing to assess end-to-end response time of event chains spanning over a set of networked devices. In this paper we develop a method to provide safe end-to-end response time taking both intra- and inter-device delivery delays into account. As a use case we study the implementation onto (single-core) ARM-cortex based devices communicating over a switched Ethernet network. For the analysis we define a generic switch model and an experimental setup allowing us to study the impact of network topology as well as 802.1Q quality of service in a mixed critical setting. Our results indicate that safe sub millisecond end-to-end response times can be obtained using the proposed approach.

Real-Time For the Masses (RTFM) is a set of languages and tools being developed to facilitate embedded software development and provide highly efficient implementations geared to static verification. The RTFM-kernel is an architecture designed to provide highly efficient and predicable Stack Resource Policy based scheduling, targeting bare metal (single-core) platforms. We contribute by introducing a platform independent timer abstraction that relies on existing RTFM-kernel primitives. We develop two alternative implementations for the ARM Cortex-M family of MCUs: a generic implementation, using the ARM defined SysTick/DWT hardware; and a target specific implementation, using the match compare/free running timers. While sacrificing generality, the latter is more flexible and may reduce overall overhead. Invariants for correctness are presented, and methods to static and run-time verification are discussed. Overhead is bound and characterized. In both cases the critical section from release time to dispatch is less than 2us on a 100MHz MCU. Queue and timer mechanisms are directly implemented in the RTFM-core language ( -core in the following) and can be included in system-wide scheduling analysis.

The IEC 61449 standard provides an outset for designing and deploying distributed control systems. Recently, a mapping from IEC 61499 to the RTFM-kernel API has been presented. This allows predictable real-time execution of IEC 61499 applications on light-weight single-core platforms. However, integrating the RTFM-kernel (bare-metal runtime) into potential deployments requires developing device drivers, protocol stacks, and the like. For this presentation, we apply the mapping from IEC 61499 to the RTFM-MoC task and resource model implemented by the RTFM-core language. The compilation from RTFM-core can be targeted to both, RTFM-kernel and the introduced runtime system RTFM-RT. In this paper, we detail the generic RTFM-RT runtime architecture, which allows RTFM-core programs to be executed on top of thread based environments. Furthermore, we discuss our implementation regarding scheduling specifics of Win32 threads (Windows) and Pthreads (Linux and Mac OS X). Using our RTFM-RT implementation for deployment, predictable IEC 61499 execution together with access to abovementioned operating system functions are achieved. For further developments, we discuss the needed scheduling options to achieve hard real-time and analysis required to eliminate deadlocks.

The IEC 61499 standard provides an executable model for distributed control systems in terms of interacting function blocks. However, the current IEC 61499 standard lacks appropriate timing semantics for the specification of timing requirements, reasoning on timing properties at the model level, and for the timing verification of a specific deployment.In this paper we address this fundamental shortcoming by proposing Real-Time-4-FUN, a real-time semantics for IEC 61499. The key property is the preservation of non-determinism, allowing us to reason on (and verify) timing properties at the model level without assuming any specific scheduling policy or stipulating specific order of execution for the deployment. This provides for a clear separation of concerns, where the designer can focus on properties of the application prior to, and separately from, deployment verification. The proposed timing semantics is backwards compatible to the current standard, thus allow for reuse of existing designs. The transitional property allows timing requirements to propagate to downstream sub-systems, and can be utilized for scheduling both at device and network level.Based on a translation to RTFM-tasks and resources, IEC 61499 models can be analyzed, compiled and executed. As a proof of concept the timing semantics has been experimentally implemented in the RTFM-core language and the accompanying (thread based) RTFM-RT run-time system.

The mainstream of embedded software development as of today is dominated by C programming. To aid the development, hardware abstractions, libraries, kernels and lightweight operating systems are commonplace. Such kernels and operating systems typically impose a thread based abstraction to concurrency. However, in general thread based programming is hard, plagued by race conditions and dead-locks.For this paper we take an alternative outset in terms of a language abstraction, RTFM-core, where the system is modelled directly in terms of tasks and resources. In compliance to the Stack Resource Policy (SRP) model, the language enforces (well-formed) LIFO nesting of claimed resources, thus SRP based analysis and scheduling can be readily applied. For the execution onto bare-metal single core architectures, the rtfm-core compiler performs SRP analysis on the model and render an executable that is deadlock free and (through RTFM-kernel primitives) exploits the underlying interrupt hardware for efficient scheduling. The RTFM-core language embeds C-code and links to C-object files and libraries, and is thus applicable to the mainstream of embedded development.However, while the language enforces well-formed resource management, control flow in the embedded C-code may violate the LIFO nesting requirement.In this paper we address this issue by lifting a subset of C into the RTFM-core language allowing arbitrary control flow at the model level. In this way well-formed LIFO nesting can be enforced, and models ensured to be correct by construction. We demonstrate the feasibility by means of a prototype implementation in the rtfm-core compiler. Additionally, we develop a set of running examples and show in detail how control flow is handled at compile time and during run-time execution.

Function Blocks provides a means to model and program industrial control systems. The recently acclaimed IEC 61499 standard allows such system models to be partitioned and executed in a distributed fashion. At device level, such models are traditionally implemented onto programmable logic controllers that underneath have an operating system and a software run-time environment which implies high resource demands. However, there is a current trend to involve small embedded systems (so called Internet of Things devices) integrated into such distributed control systems. To this end, we seek to address the outsets for real-time execution of Function Block based designs onto light-weight controllers (MCUs) with limited resources (memory and CPU). Furthermore, we propose a mapping of the Function Block execution semantics onto the RTFM-kernel, and discuss opportunities for off-line (design time) analysis with respect to response time, overall schedulability and memory requirements.

Function Blocks provides a means to model and program industrial control systems. The recently acclaimed IEC 61499 standard allows such system models to be partitioned and executed in a distributed fashion. At device level, such models are traditionally implemented onto programmable logic controllers and industrial PCs. In this paper, we discuss work in progress on developing a mapping allowing to implement a subset of IEC 61499 models onto light-weight embedded devices (MCUs). We propose and detail an event semantics, and its mapping to the notions of task and resources for Stack Resource Policy based analysis and scheduling. Moreover, we show how the proposed mapping can be efficiently implemented under the RTFM-kernel. Finally we outline a prototype tool-chain and discuss related, ongoing and future work.