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.

Remote attestation consists of generating evidence of a system’s integrity via measurements and reporting the evidence to a remote party for appraisal in a form that can be trusted. The parties that exchange information must agree on formats and protocols. We assert there is a large variety of patterns of interactions among appraisers and attesters of interest. Therefore, it is important to standardize on flexible mechanisms for remote attestation. We make our case by describing scenarios that require the exchange of evidence among multiple parties using a variety of message passing patterns. We show cases in which changes in the order of evidence collection result in important differences to what can be inferred by an appraiser. We argue that adding the ability to negotiate the appropriate kind of attestation allows for remote attestations that better adapt to a dynamically changing environment. Finally, we suggest a language-based solution to taming the complexity of specifying and negotiating attestation procedures.

This work examines the use of model checking techniques to verify system-level security properties of a collection of interacting virtual machines. Specifically, we examine how local access control policies implemented in individual virtual machines and a hypervisor can be shown to satisfy global access control constraints. The SAL model checker is used to model and verify a collection of stateful domains with protected resources and local MAC policies attempting to access needed resources from other domains. The model is described along with verification conditions. The need to control state-space explosion is motivated and techniques for writing theorems and limiting domains explored. Finally, analysis results are examined along with analysis complexity.

The software defined radios movement is revolutionizing radio design by separating function from specific implementation. Like traditional software systems, software defined radio systems use a common operational definition that may be realized across numerous platforms. This paper describes initial efforts at realizing the promise of software defined radios by synthesizing radios to multiple implementation fabrics from a common Rosetta specification. We outline the approach by describing specifications used at each abstraction level, the operations implemented to synthesize radios, and various analysis techniques used to provide assurance in the resulting radio.

Modular Monadic Semantics (MMS) is a well-known mechanism for structuring modular denotational semantic definitions for programming languages. The principal attraction of MMS is that families of language constructs can be independently specified and later combined in a mix-and-match fashion to create a complete language semantics. This has proved useful for constructing formal, yet executable, semantics when prototyping languages. In this work we demonstrate that MMS has an additional software engineering benefit. Rather than composing semantics for various language constructs, we can use MMS to compose various differing semantics for the same language constructs. We describe algebra combinators, the principal vehicle for achieving this reuse, along with a series of applications of the technique for common language processing tasks.

Modular monadic semantics (MMS) is a well-known technique for structuring modular denotational semantic definitions. Families of language constructs are independently defined using syntactic functors and semantic algebras that can be combined in a mix-and-match fashion to create complete language definitions. We introduce InterpreterLib, a Haskell library that implements and extends MMS techniques for writing composable analyses. In addition to modular analyses composition, InterpreterLib provides algebra combinators, explicit algebra semantics, preprocessors for boiler plate generation and generic programming techniques adapted to language analysis. The key benefits of these features are reliability, increased code reuse via modularity and the ability to rapidly retarget component analyses.

Current formal software engineering methodologies provide a vast array of languages for specifying correctness properties, as well as a wide assortment automated tools that aid in the verification of specified properties. Unfortunately, the implementation of each such tool requires an early commitment to a particular methodology and language, in terms of both high-level semantic concerns and the lower-level syntactic representations of properties and proofs. In this paper, we present Prufrock, a novel approach to automated reasoning systems, which abstracts semantic concerns over entire classes of potential implementation languages. Prufrock utilizes polytypic programming techniques to create independent, reusable modules defining proof in different logics, independent of the language used to represent formulae in the logic, as well as the exact implementation of low-level prover functionality.

A continuing challenge for software designers is to develop efficient and cost-effective software implementations. Many see software reuse as a potential solution; however, the cost of reuse tends to outweigh the potential benefits. The costs of software reuse include establishing and maintaining a library of reusable components, searching for applicable components to be reused in a design, as well as adapting components toward a proper implementation. We introduce SPARTACAS, a framework for automating specification-based component retrieval and adaptation that has been successfully applied to synthesis of software for embedded and digital signal processing systems. Using specifications to abstractly represent implementations allows automated theorem-provers to formally verify logical reusability relationships between specifications. These logical relationships are used to evaluate the feasibility of reusing the implementations of components to implement a problem. Retrieving a component that is a complete match to a problem is rare. It is more common to retrieve a component that partially satisfies the requirements of a problem. Such components have to be adapted. Rather than adapting components at the code level, SPARTACAS adapts the behavior of partial matches by imposing interactions with other components at the architecture level. A subproblem is synthesized that specifies the missing functionality required to complete the problem; the subproblem is used to query the library for components to adapt the partial match. The framework was implemented and evaluated empirically, the results suggest that automated adaptation using architectures successfully promotes software reuse, and hierarchically organizes a solution to a design problem.

Reuse is a sound and practical design technique in many engineering disciplines. Although successful instances of software reuse are becoming more common, the cost of reuse tends to outweigh the potential benefits. The costs of software reuse include establishing and maintaining a library of reusable components, searching for applicable components to be reused, as well as adapting components toward a solution to a design problem. In this paper, we present a framework, called SPARTACAS, for automating specification-based component retrieval and adaptation. Components that partially satisfy the constraints of a design problem are adapted using adaptation architectures. Adaptation architectures modify the behavior of a software component by imposing interactions with other components. Based on the functionality specified in the problem and the partially-matched component, a sub-problem that specifies the missing functionality is synthesized. The sub-problem is used to query the library for components for adaptation. The framework was implemented and evaluated empirically, the results suggest that automated adaptation using architectures successfully promotes software reuse, and hierarchically organizes a solution to a design problem.

Modern systems engineering mandates the integration of heterogeneous models in systems design and analysis. Analysis of modern, mixed technology systems requires the horizontal integration of heterogeneous models for predictive analysis. The ever increasing role of performance constraints such as power, cost and throughput requires vertical integration of heterogeneous component models describing different requirements facets. The Rosetta (Alexander et al., 2000; 2001) specification language has been developed to address the issue of specification and analysis of heterogeneous models. We describe the semantics of Rosetta's specification composition in the context of systems level requirements modeling.

The paper describes a formal framework developed using the Prototype Verification System (PVS) to model and verify distributed simulation kernels based on the Time Warp paradigm. The intent is to provide a common formal base from which domain specific simulators can be modeled, verified, and developed. PVS constructs are developed to represent basic Time Warp constructs. Correctness conditions for Time Warp simulation are identified, describing causal ordering of event processing and correct rollback processing. The PVS theorem prover and type-check condition system are then used to verify all correctness conditions. In addition, the paper discusses the framework's reusability and extensibility properties in support of specification and verification of Time Warp extensions and optimizations.

As systems become increasingly complex and existing methodologies become insufficient to handle the complexity, the design community is beginning to look at formal methods for a possible solution. Techniques involving a limited use of formal techniques (such as semi-formal methods and equivalence checking) have given a glimpse of what full usage of formal techniques can achieve. For the use of formal methods to be a widely accepted methodology among designers, it must provide the designers with the capabilities of structuring specifications in a manner similar to the structuring they are used to using with programming languages. In this paper, we provide a description of the structuring capabilities of VSPEC (VHDL SPECification), a requirements specification language for VHDL. These capabilities include the use of multiple pre- and post-condition pairs within a single specification and combination of specifications using common Boolean operators.

This paper presents BENTON, a prototype system demonstrating task analysis and multi-agent reasoning applied to formal specification synthesis. BENTON transforms specifications written as attribute-value pairs into Larch Modula-3 interface language and Larch Shared Language specifications. BENTON decomposes the software specification design task into synthesis, analysis and evaluation subtasks. Each subtask is assigned a specific design method based on problem and domain characteristics. This task analysis is achieved using blackboard knowledge sources and multi-agent reasoning employing design plans to implement different problem solving methods. Knowledge sources representing different problem solving methodologies monitor blackboard spaces and activate when they are applicable. When executed, Design plans send subtasks to agents that select from available problem solving methodologies. BENTON agents and knowledge sources use case-based reasoning, schemata-based reasoning and procedure execution as their fundamental reasoning methods. This paper presents an overview of the BENTON design model, its agent architecture and plan execution capabilities, and two annotated examples of BENTON problem solving activities.

Scaling formal methods to large, complex systems requires methods of modeling systems at high levels of abstraction. In this paper, we describe such a method for specifying system requirements at the software architecture level. An architecture represents a way breaking down a system into a set of interconnected components. We use architecture theories to specify the behavior of a system in terms of the behavior of its components via a collection of axioms. The axioms describe the effects and limits of component variation and the assumptions a component can make about the environment provided by the architecture. As a result of the method the verification of the basic architecture can be separated from the verification of the individual component instantiations. We present an example of using architecture theories to model the task coordination architecture of a multi-threaded plan execution system.