This paper describes a method for using property definition templates to support automatic analysis of source code for application-specific security properties. The method is illustrated on an example data flow property of a C program.

Recently, software practitioners, using model-based engineering and similar methods, have begun developing software from models. After creating a model of the required system behavior, a developer can obtain assurance of the model by validating that it captures the intended behavior and verifying that it satisfies critical properties. Invariants are important to both validation, as a check that the model's behavior matches the intended behavior, and verification, as auxiliaries in proving critical system properties, either automatically or with human guidance. A common approach to discovering invariants is to propose and then check candidate invariants. In contrast, our invariant generation techniques deduce invariants directly from the specification of a model. This paper presents more powerful versions of our earlier techniques for invariant generation and illustrates their utility for a real-world AirLock system.

A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This article describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, the security property of interest is represented formally and a compact security model, containing only information needed to reason about the policy, is constructed. To reduce the cost of verification, the code to be verified is partitioned into three categories: Only the first category, less than 10% of the code, requires requires substantial effort to verify; the proof of the other two categories is relatively trivial. Our approach was developed to support a Common Criteria evaluation of the separation kernel of an embedded software system. This article describes 1) our techniques and theory for verifying the kernel code and 2) the artifacts produced: a Top Level Specification (TLS), a formal statement of the security property, a mechanized proof that the TLS satisfies the property, the partitioning of the code, and a demonstration that the code conforms to the TLS. The article also presents the formal argument that the kernel code conforms to the TLS and consequently satisfies the security property.

Based on our recent experience in four projects, each focused on either security-critical or safety-critical software, this paper evaluates several notions, widely held by RE researchers, for their utility in practical software development. It describes four notions which in our view work in practice and five others which do not.

Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for verification. This paper describes a novel and practical approach to formally establishing the security of code. The approach begins with a well-defined set of security properties and, based on the properties, constructs a compact security model containing only information needed to rea-son about the properties. Our approach was formulated to provide evidence for a Common Criteria evaluation of an embedded soft-ware system which uses a separation kernel to enforce data separation. The paper describes 1) our approach to verifying the kernel code and 2) the artifacts used in the evaluation: a Top Level Specification (TLS) of the kernel behavior, a formal definition of dataseparation, a mechanized proof that the TLS enforces data separation, code annotated with pre- and postconditions and partitioned into three categories, and a formal demonstration that each category of code enforces data separation. Also presented is the formal argument that the code satisfies the TLS.

Timed I/O Automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The TIOA toolkit, currently under development, is aimed at supporting system development based on TIOA specifications. The TIOA toolkit is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on modeling of timed systems with TIOA and the TAME-based theorem proving support provided in the toolkit, for proving system properties, including timing properties. Several examples are provided by way of illustration.

We focus on how to capture common specification and proof patterns in PVS in order to tailor PVS for the verification of a particular class of systems. The use of specification templates can simplify the development of PVS strategies that correspond to proof steps that recur in proofs of specific classes of system properties.

We have developed an approach to organizing automaton specifications in which a reference variable captures the essential state and shadow variables are used to facilitate expressiveness. We have applied our approach in specifying automaton models for three different examples: TESLA protocol, SELinux security policies and leader election for IEEE 1394. In all three cases the resulting specification bears an obvious close relationship to the actual system being modeled.

To date, the tabular based SCR (Software Cost Reduction) method has been applied mostly to the development of embedded control systems. The paper describes the successful application of the SCR method, including the SCR* toolset, to a different class of system, a COMSEC (Communications Security) device called CD that must correctly manage encrypted communications. The paper summarizes how the tools in SCR* were used to validate and to debug the SCR specification and to demonstrate that the specification satisfies a set of critical security properties. The development of the CD specification involved many tools in SCR*: a specification editor, a consistency checker, a simulator, the TAME interface to the theorem prover PVS, and various other analysis tools. Our experience provides evidence that use of the SCR* toolset to develop high quality requirements specifications of moderately complex COMSEC systems is both practical and low cost.

Although most typically used in other contexts, program transformations can simplify program verification by transforming a program containing complex language features into a semantically equivalent program containing only simpler language features. The proof of the transformed program can then be performed using a set of proof rules for only the simpler features. There are tradeoffs between the transformational approach and the standard approach to program verification with regard to proof understandability and compactness of programs and assertions, establishing soundness of the program verification method, and providing mechanized support for the method. The transformational approach has clear advantages in some of these aspects. This paper illustrates this transformational approach by considering proof rules for escape statements in iterative constructs, and discusses the tradeoffs with respect to its use. It also suggests how the approach can be applied to other language constructs, including some involving concurrency, and to solving some problems connected with the development of Hoare axiomatizations. Copyright © 1999 John Wiley & Sons, Ltd.

Exposing inconsistencies can uncover many defects in software specifications. One approach to exposing inconsistencies analyzes two redundant specifications, one operational and the other property-based, and reports discrepancies. This paper describes a "practical" formal method, based on this approach and the SCR (software cost reduction) tabular notation, that can expose inconsistencies in software requirements specifications. Because users of the method do not need advanced mathematical training or theorem-proving skills, most software developers should be able to apply the method without extraordinary effort. This paper also describes an application of the method which exposed a safety violation in the contractor-produced software requirements specification of a sizable, safety-critical control system. Because the enormous state space of specifications of practical software usually renders direct analysis impractical, a common approach is to apply abstraction to the specification. To reduce the state space of the control system specification, two "pushbutton" abstraction methods were applied, one which automatically removes irrelevant variables and a second which replaces the large, possibly infinite, type sets of certain variables with smaller type sets. Analyzing the reduced specification with the model checker Spin uncovered a possible safety violation. Simulation demonstrated that the safety violation was not spurious but an actual defect in the original specification.

In a previous paper, M. Archer et al. (1990) presented a tool for the rapid prototyping of operating systems based on an executable template operating system specification. By extending the template specification, a designer can generate a rapid prototype of a specific operating system. The template specification consists of sorts (object classes) arranged in a hierarchy of three kinds, where the design decisions made in the template for each kind are in some sense more general than those made for its successor kind. The FASE (final algebra specification and execution) system language was used as the language for the specification. It is the authors' belief that the SRM template is general enough to be used as a basis for rapid prototyping nearly any non-distributed operating system at the system call level. It is important to test this belief, and to show that the speed of prototype development and the execution speed of a rapid prototype are great enough for the development of a prototype to be useful for testing the properties of a design. The authors answer these questions, demonstrate the usefulness of having a rapid prototype of an operating system, and evaluate the template methodology in general.>

Probably the most important characteristic of a user interface is its 'look and feel'. One can model the 'look and feel' of user interfaces via rapid prototyping. However, the behavior of a particular user interface is greatly influenced by the particular user interface management system (UIMS) upon which it is built, so it is necessary to prototype an interface with regard to a particular user interface management system. Moving an application and its user interface to a different UIMS may result in a user interface that behaves in a substantially different manner. The authors describe a methodology that may be used to develop a UIMS prototype using a template. This template will assist developers not only in developing new UIMSs but in evaluating the behavior of user interfaces when the underlying UIMS changes.>

Rapid prototyping of many classes of systems can be facilitated by starting from an executable template specification appropriate to that class. A system template serves several useful purposes. It organizes ones thinking about the particular system to be specified, and speeds the specification process by pre-specifying structures and operations common to all systems in a class. If executable, it can be developed into a system prototype. Though beyond the scope of this paper, it can organize proofs of properties of the specification and its implementations by making it possible to isolate the relevant proof obligations. The authors templates have an additional property: they classify sub-specifications according to "kinds" that needs to be completed differently. The authors illustrate rapid prototyping from a template for operating systems, specifically showing how to obtain a rapid prototype of the MINIX system. This approach may also be useful for other classes of systems, such as architectures.>