Cyber-security has emerged as a pressing issue for transportation systems. Studies have shown that attackers can attack modern vehicles from a variety of interfaces and gain access to the most safety-critical components. Such threats become even broader and more challenging with the emergence of vehicle-to-vehicle (V2V) and vehicle-to-infrastructure (V2I) communication technologies. Addressing the security issues in transportation systems requires comprehensive approaches that encompass considerations of security mechanisms, safety properties, resource constraints, and other related system metrics. In this work, we propose an integrated framework that combines hybrid modeling, formal verification, and automated synthesis techniques for analyzing the security and safety of transportation systems and carrying out design space exploration of both in-vehicle electronic control systems and vehicle-to-vehicle communications. We demonstrate the ideas of our framework through a case study of cooperative adaptive cruise control.
Natarajan Shankar
SRI Author
A Framework for High-Assurance Quasi-Synchronous Systems
The design of a complex cyber-physical system is centered around one or more models of computation (MoCs). These models define the semantic framework within which a network of sensors, controllers, and actuators operate and interact with each other. In this paper, we examine the foundations of a quasi-synchronous model of computation Our version of the quasi-synchronous model is inspired by the Robot Operating System (ROS). It consists of nodes that encapsulate computation and topic channels that are used for communicating between nodes. The nodes execute with a fixed period with possible jitter due to local clock drift and scheduling uncertainties, but are not otherwise synchronized. The channels are implemented through a mailbox semantics. In each execution step, a node reads its incoming mailboxes, applies a next-step operation to update its local state, and writes to all its outgoing mailboxes. The underlying transport mechanism implements the mailbox-to-mailbox data transfer with some bounded latency. Messages can be lost if a mailbox is over-written before it is read. We prove a number of basic theorems that are useful for designing robust high-assurance cyber-physical systems using this simple model of computation. We show that depending on the relative rates of the sender and receiver, there is a bound on the number of consecutive messages that can be lost. By increasing the mailbox queue size to a given bound, message loss can be eliminated. We demonstrate that there is a bound on the age of inputs that are used in any processing step. This in turn can be used to bound the end-to-end sense-control-actuate latency. We illustrate how these theorems are useful in designing and verifying a thermostat-based heating system. Our proofs have been mechanically verified using the Prototype Verification System (PVS).
The Semantics of Datalog for the Evidential Tool Bus
The Evidential Tool Bus (ETB) is a distributed framework for tool integration for the purpose of building and maintaining assurance cases. ETB employs Datalog as a metalanguage both for defining workflows and representing arguments. The application of Datalog in ETB differs in some significant ways from its use as a database query language. For example, in ETB Datalog predicates can be tied to external tool invocations. The operational treatment of such external calls is more expressive than the use of built-in predicates in Datalog. We outline the semantic characteristics of the variant of Datalog used in ETB and describe an abstract machine for evaluating Datalog queries.
The Gradual Verifier
Static verification traditionally produces yes/no answers. It either provides a proof that a piece of code meets a property, or a counterexample showing that the property can be violated. Hence, the progress of static verification is hard to measure. Unlike in testing, where coverage metrics can be used to track progress, static verification does not provide any intermediate result until the proof of correctness can be computed. This is in particular problematic because of the inevitable incompleteness of static verifiers.
To overcome this, we propose a gradual verification approach, GraVy. For a given piece of Java code, GraVy partitions the statements into those that are unreachable, or from which exceptional termination is impossible, inevitable, or possible. Further analysis can then focus on the latter case. That is, even though some statements still may terminate exceptionally, GraVy still computes a partial result. This allows us to measure the progress of static verification.We present an implementation of GraVy and evaluate it on several open source projects.
Reverse Engineering Digital Circuits Using Structural and Functional Analyses
Integrated circuits (ICs) are now designed and fabricated in a globalized multivendor environment making them vulnerable to malicious design changes, the insertion of hardware Trojans/malware, and intellectual property (IP) theft. Algorithmic reverse engineering of digital circuits can mitigate these concerns by enabling analysts to detect malicious hardware, verify the integrity of ICs, and detect IP violations. In this paper, we present a set of algorithms for the reverse engineering of digital circuits starting from an unstructured netlist and resulting in a high-level netlist with components such as register files, counters, adders, and subtractors. Our techniques require no manual intervention and experiments show that they determine the functionality of >45% and up to 93% of the gates in each of the test circuits that we examine. We also demonstrate that our algorithms are scalable to real designs by experimenting with a very large, highly-optimized system-on-chip (SOC) design with over 375000 combinational elements. Our inference algorithms cover 68% of the gates in this SOC. We also demonstrate that our algorithms are effective in aiding a human analyst to detect hardware Trojans in an unstructured netlist.
Accountable Clouds
An increasing number of organizations are migrating their critical information technology services, from healthcare to business intelligence, into public cloud computing environments. However, even if cloud technologies are continuously evolving, they still have not reached a maturity level that allows them to provide users with high assurance about the security of their data beyond existent service level agreements (SLAs). To address this limitation, we propose a suite of mechanisms that enhances cloud computing technologies with more assurance capabilities. Assurance becomes a measurable property, quantified by the volume of evidence to audit and retain in a privacy-preserving and nonrepudiable fashion. By proactively collecting potential forensic evidence, the cloud becomes more accountable, while providing its regular services. In the case of a security breach, the cloud provides the appropriate reactive security framework for validating or repudiating claims. Moreover, different levels of assurance relate to different levels of storage and privacy protection requested by users, leading to an assurance-based price model for cloud services.
JBernstein: A Validity Checker for Generalized Polynomial Constraints
SRI Authors: Natarajan Shankar
WordRev: Finding Word-Level Structures in a Sea of Bit-Level Gates
Systems are increasingly being constructed from off-the-shelf components acquired through a globally distributed and untrusted supply chain. Often only post-synthesis gate-level netlists or actual silicons are available for security inspection. This makes reasoning about hardware trojans particularly challenging given the enormous scale of the problem. Currently, there is no mature methodology that can provide visibility into a bit-level design in terms of high-level components to allow more comprehensive analysis. In this paper, we present a systemic way of automatically deriving word-level structures from the gate-level netlist of a digital circuit. Our framework also provides the possibility for a user to specify sequences of word-level operations and it can extract the collection of gates corresponding to those operations. We demonstrate the effectiveness of our approach on a system-on-a-chip (SoC) design consisting of approximately 400,000 IBM 12SOI cells and several open-source designs.
