Confidentiality is a crucial security property for many critical applications. As a response to the discovery of numerous micro-architectural side channel attacks such as Spectre, allowing an attacker to extract secret information in pernicious ways, the notion of hardware/software contracts was proposed to formalise the guarantees provided by the hardware to the software. In this paper, we propose to extend this notion to include the guarantees provided by the operating system (OS), so far unspecified in such contracts. We formalize an attacker model adapted to a typical execution model on a shared platform. More precisely, we formalize common thread and memory management policies provided by the OS on top of a hardware model and explore the consequences of potential leaks emerging on such a platform. Our investigation shows that the OS policies play a crucial role in providing security guarantees to code processing sensitive data and thus have to be taken into consideration when writing such code through platform contracts.

Moving Target Defense (MTD) is a promising de-fense technique that aims to break the asymmetry between attacker and defender by reconfiguring a system's assets. When used in a critical embedded system, non-functional constraints limit the set of usable MTD techniques, therefore limiting the entropy of reconfigurations. It is therefore necessary to compute an optimal moving target strategy in order to reduce the time between reconfigurations, while managing their impact on the quality of service provided to users. In this paper, we propose a game-theoretic approach to define an optimal moving target defense strategy. Our approach translates risk analysis parame-ters into a Bayesian Stackelberg game, which we translate to a mixed integer linear program. We validate our approach on an industrial case study from the automotive domain, showing the practical usability of our approach. In further experiments, we assess the scalability of our method, as well as the solution's stability in case new vulnerabilities are discovered after the deployment of the system.

Hardware Trojan Horses and active fault attacks are a threat to the safety and security of electronic systems. By such manipulations, an attacker can extract sensitive information or disturb the functionality of a device. Therefore, several protections against malicious inclusions have been devised in recent years. A prominent technique to detect abnormal behavior in the field is run-time verification. It relies on dedicated monitoring circuits and on verification rules generated from a set of temporal properties. An important question when dealing with such protections is the effectiveness of the protection against unknown attacks. In this paper, we present a methodology based on automatic generation of monitoring and formal verification techniques that can be used to validate and analyze the quality of a set of temporal properties when used as protection against generic attackers of variable strengths.

In this paper we present a hardware based solution to verify simultaneously Code and Control-Flow Integrity (CCFI), aiming at protecting microcontrollers against both cyber-and physical attacks. This solution is non-intrusive as it does not require any modification of the CPU core. It relies on two additional hardware blocks external to the CPU: The first one – called CCFI-cache – acts as a dedicated cache for the storage of information to check the code and control-flow integrity, and the second one – CCFI-checker – performs control-flow and code integrity verification. Based on a RISC-V platform implementation, we show that the proposed scheme is able to perform online CCFI validation at the price of a small hardware area overhead and doubling the size of the. text section. In most cases, the impact on the run-time performance is on average 32 percent, offering for the first time a generic and practical hardware-enabled cyber-security solution.

The complexity of today's embedded and cyber-physical systems is rapidly increasing and makes the consideration of higher levels of abstraction during the design process inevitable. In this context, the impact of modeling languages such as UML and its profiles such as MARTE is growing. Here, CCSL provides a formal description of timing constraints which have to be enforced on the considered system. This builds the basis for many further design steps and can be used e. g. for checking the consistency of the specification, for code generation, or for proving whether the time constraints have correctly been implemented at lower abstraction levels. However, most of the approaches available thus far usually focus on sole design tasks only -- often even without an explicit consideration of the system's functional behavior. In this work, we are aiming for overcoming this drawback by providing a method to automatically generate a generic representation of a set of clock constraints in terms of a transition relation. Afterwards, the resulting transition relation can easily be utilized for the above mentioned design tasks. A discussion on the applicability of the generic description as well as an exemplary evaluation shows the promise of the proposed generic representation.

The application of built-to-order embedded hardware designs in safety critical systems requires a high design quality and robustness during operation. Flawless execution of the involved software can be compromised by malfunctioning hardware components or by software-induced errors. Furthermore, intellectual property (IP) tends to become unavoidable in modern hardware designs. Any unexpected behavior of IP components may cause unrecoverable system errors. In order to construct correct and safe systems from unverified and potentially malicious components, we propose a system integration approach which encapsulates IP blocks in verifiable container modules. The synthesis of these container modules is driven by a domain specific language (DSL) augmented with sequential extended regular expressions (SEREs). The approach is demonstrated by showing the synthesis of an effective countermeasure against software-induced memory disturbance errors.

Decimal floating-point is a relatively recent addition to the IEEE standard (IEEE Std 754-2008). There exist few verification techniques that can check whether software libraries or hardware designs are in compliance with the standard. Our work presents a verification method to verify implementations of the decimal floating-point square root operation. We present an effective simulation based verification technique using test cases that verify the corner cases of the operation. The test cases are generated by solving constraints describing these corner cases with a dedicated constraint solver. The generated test cases proved their usefulness by finding severe bugs in two well-tested designs.

Modeling languages such as SysML provide various description means for a precise specification of the desired system. As a system model typically uses multiple diagram types focusing on different aspects, it is crucial to keep them consistent to each other. In this paper, we propose a verification methodology which ensures the consistency between activity diagrams as blueprints for the implementation and their contracts from a block definition diagram. For this purpose, activity diagrams are transformed to OCL constraints that can be checked against pre- and postconditions. The proposed approach is evaluated in a case study based on an industrial specification.

For the design of complex systems, formal modeling languages such as UML or SysML find significant attention. The typical model-driven design flow assumes thereby an initial (abstract) model which is iteratively refined to a more precise description. During this process, new errors and inconsistencies might be introduced. In this paper, we propose an automatic method for verifying the consistency of refinements in UML or SysML. For this purpose, a theoretical foundation is considered from which the corresponding proof obligations are determined. Afterwards, they are encoded as an instance of Satisfiability Modulo Theories (SMT) and solved using proper solving engines. The practical use of the proposed method is demonstrated and compared to a previously proposed approach.

The automatic verification of designs is a challenging task and of high interest due to increasing time-to-market constraints. In this paper, we focus on the verification of bus bridges which are used in many hardware systems to connect two buses running different protocols. We developed an approach to assist the automatic generation of properties from the protocol specification for the formal verification of bus bridges. The technical contribution is that the final set of the verification suite is functionally complete in respect to the underlying verification tool which shows the absence of any verification holes. The approach uses an abstract model of bus bridges in terms of state machines which enables a generic work flow. In experimental evaluations we applied the approach to bus bridges based on the OCP/IP protocol family.

Today for System-on-Chips (SoCs) companies Electronic System Level(ESL) design is the established approach. Abstraction and standardized communication interfaces based on SystemC Transaction Level Modeling (TLM) have become the core component for ESL design. The abstract models in ESL flows are stepwise refined down to hardware. In this context verification is the major bottleneck: After each refinement step the resulting model is simulated again with the same testbench. The simulation results have to be compared to the previous results to check the functional equivalence of both models. For models at lower levels of abstraction strong approaches exist to formally prove equivalence. However, this is not possible here due to the TLM abstraction. Hence, in practice equivalence checking in ESL flows is based on simulation. Since implementing the necessary verification environment requires a huge effort, we propose an equivalence checking framework in this paper. Our framework allows to easily compare variable accesses in different SystemC models. Therefore, the two models are co-simulated using a client-server architecture. In combination with multi-threading our approach is very efficient as shown by the experiments. In addition, the time required for debugging is reduced by the framework since the respective source code references where the variable accesses did not match are presented to the user.

Verification is a major issue in circuit and system design. Formal methods like bounded model checking (BMC) can guarantee a high quality of the verification. There are several techniques that can check if a set of formal properties forms a complete specification of a design. But, in contrast to simulation-based methods, like random testing, formal verification requires a detailed knowledge of the design implementation. Finding the correct set of properties is a tedious and time consuming process. In this paper, two techniques are presented that provide automatic support for writing properties in a quality-driven BMC flow. The first technique can be used to analyze properties in order to remove redundant assumptions and to separate different scenarios. The second technique - inverse property checking - automatically generates valid properties for a given expected behavior. The techniques are integrated with a coverage check for BMC. Using the presented techniques, the number of iterations to obtain full coverage can be reduced, saving time and effort.

Equivalence checking and property checking are powerful techniques to detect error traces. Debugging these traces is a time consuming design task where automation provides help. In particular, debugging based on Boolean satisfiability (SAT) has been shown to be quite efficient. Given some error traces, the algorithm returns fault candidates. But using random error traces cannot ensure that a fault candidate is sufficient to explain all erroneous behaviors. Our approach provides a more accurate diagnosis by iterating the generation of counterexamples and debugging. This increases the accuracy of the debugging result and yields more valuable counterexamples. As a consequence less time consuming manual iterations between verification and debugging are required - thus the debugging productivity increases.

In the context of formal verification Bounded Model Checking (BMC) has shown to be very powerful for large industrial designs. BMC is used to check whether a circuit satisfies a temporal property or not. Typically, such a property is formulated as an implication. In the antecedent of the property the verification engineer specifies the assumptions about the design environment and joins the respective expressions by logical AND. However, the overall conjunction may have no solution, i.e. the antecedent is contradictory. Since in this case a property trivially holds this situation has to be avoided. Furthermore, the root cause of a contradictory antecedent has to be identified which is a manual and very time-consuming process. In this paper we propose a fully automatic approach for presenting all reasons of a contradictory antecedent to the verification engineer, i.e. the approach pinpoints to the sub-expressions in the antecedent that form a contradiction. Hence, our approach reduces the debugging time of a contradictory antecedent significantly.

Formal verification is an important issue in circuit and system design. In this context, bounded model checking (BMC) is one of the most successful techniques. However, even if all the specified properties can be verified, it is difficult to determine whether they cover the complete functional behavior of a design. We propose a practical approach to analyze coverage in BMC. The approach can easily be integrated in a BMC tool with only minor changes. In our approach, a coverage property is generated for each important signal. If the considered properties do not describe the signal's entire behavior, the coverage property fails, and a counter example is generated. From the counter example, an uncovered scenario can be derived. This way, the approach also helps in design understanding. We demonstrate our method for a reduced instruction set computer (RISC) CPU. First, the coverage of the block-level verification is considered. Second, it is demonstrated how the technique can be applied on a higher level. Therefore, we investigate the instruction set verification of the RISC CPU. The experiments show that the costs for coverage analysis are comparable to the verification costs. Based on the results, we identified coverage gaps during the verification. We were able to close all of them and achieved 100% functional coverage in total.

Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the functional correctness. But in embedded system design the integration of software components becomes more and more important. In this paper we present an integrated approach for formal verification of hardware and software. The approach is demonstrated on a RISC CPU. The verification is based on bounded model checking. Besides correctness proofs of the underlying hardware the hardware/software interface and programs using this interface can be formally verified.