1998

Archer, Myla M., Heitmeyer, Constance L., and Sims, Steve, "TAME: A PVS Interface to Simplify Proofs for Automata Models," UITP '98, July 1998. PostScript, PDF

Although a number of mechanical provers have been introduced and applied widely by academic researchers, these provers are rarely used in the practical development of software. For mechanical provers to be used more widely in practice, two major barriers must be overcome. First, the languages provided by the mechanical provers for expressing the required system behavior must be more natural for software developers. Second, the reasoning steps supported by mechanical provers are usually at too low and detailed a level and therefore discourage use of the prover. To help remove these barriers, we are developing a system called TAME, a high-level user interface to PVS for specifying and proving properties of automata models. TAME provides both a standard specification format for automata models and numerous high-level proof steps appropriate for reasoning about automata models. In previous work, we have shown how TAME can be useful in proving properties about systems described as Lynch-Vaandrager Timed Automata models. TAME has the potential to be used as a PVS interface for other specification methods that are specialized to define automata models. This paper first describes recent improvements to TAME, and then presents our initial results in using TAME to provide theorem proving support for the SCR (Software Cost Reduction) requirements method, a method with a wide range of other mechanized support.

Archer, Myla M. and Heitmeyer, Constance L. "Mechanical Verification of Timed Automata: A Case Study," NRL Memorandum Report 5546-98-8180, April, 1998. PostScript, PDF

This report describes the results of a case study on the feasibility of developing and applying mechanical methods, based on the proof system PVS, to prove propositions about real-time systems specified in the Lynch-Vaandrager timed automata model. In using automated provers to prove propositions about systems described by a specific mathematical model, both the proofs and the proof process can be simplified by exploiting the special properties of the mathematical model. Because both specifications and methods of reasoning about them tend to be repetitive, the use of a standard template for specifications, accompanied by standard shared theories and standard proof strategies or tactics, is often feasible. Presented are the PVS specification of three theories that underlie the timed automata model, a template for specifying timed automata models in PVS, and an example of its instantiation. Both hand proofs and the corresponding PVS proofs of two propositions are provided to illustrate how these can be made parallel at different degrees of granularity. Our experience in applying PVS to specify and reason about real-time systems modeled as timed automata is also discussed. The methods for reasoning about timed automata in PVS developed in the study have evolved into a system called TAME (Timed Automata Modeling Environment). A summary of recent developments regarding TAME is provided. A shorter version of the report was presented at the 1996 Real-Time Applications Symposium.

Gray, James W., Syverson, Paul F., "A logical approach to multilevel security of probabilistic systems," Distributed Computing, v. 11, n. 2, 1998. Postscript, PDF

We set out a modal logic for reasoning about multilevel security of probabilistic systems. This logic contains expressions for time, probability, and knowledge. Making use of the Halpern-Tuttle framework for reasoning about knowledge and probability, we give a semantics for our logic and prove it is sound. We give two syntactic definitions of perfect multilevel security and show that their semantic interpretations are equivalent to earlier, independently motivated characterizations. We also discuss the relation between these characterizations of security and between their usefulness in security analysis.

Heimdahl, Mats P.E., Heitmeyer, Constance L. "Formal Methods for Developing High Assurance Computer Systems: Working Group Report." Proceedings, Second IEEE Workshop on Industrial-Strength Formal Techniques (WIFT'98), Boca Raton, FL, Oct. 19, 1998. PostScript, PDF

This paper presents the results of a discussion conducted at the Workshop on Industrial-Strength Formal Techniques in October 1998 on the topic, "Formal Methods for Developing High Assurance Systems." It addresses three issues: the uses of formal methods in software development, the barriers to the use of formal methods in software development, and approaches to overcoming the barriers.

Heitmeyer, Constance L., "On the Need for 'Practical' Formal Methods," Formal Techniques in Real-Time and Real-Time Fault-Tolerant Systems, Proc., 5th Intern. Symposium (FTRTFT'98), Lyngby, Denmark, September 14-18, 1998, LICS 1486, pp. 18-26, (invited paper). PostScript, PDF

A controversial issue in the formal methods community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method. A fundamental assumption of this paper is that formal methods research has produced several classes of analysis that can prove useful in software development. However, to be useful to software practitioners, most of whom lack advanced mathematical training and theorem proving skills, current formal methods need a number of additional attributes, including more user-friendly notations, completely automatic (i.e., pushbutton) analysis, and useful, easy to understand feedback. Moreover, formal methods need to be integrated into a standard development process. I discuss additional research and engineering that is needed to make the current set of formal methods more practical. To illustrate the ideas, I present several examples, many taken from the SCR (Software Cost Reduction) requirements method, a formal method that software developers can apply without theorem proving skills, knowledge of temporal and higher order logics, or consultation with formal methods experts.

C. Heitmeyer, J. Kirby, B. Labaw and R. Bharadwaj, "SCR*: A Toolset for Specifying and Analyzing Software Requirements," Proc. Computer-Aided Verification, 10th Ann. Conf. (CAV'98), Vancouver, Canada, 1998. PostScript, PDF

A controversial issue in the formal methods community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method and its support tools. This paper describes the SCR (Software Cost Reduction) tools, part of a "practical" formal method--a method with a solid mathematical foundation that software developers can apply without theorem proving skills, knowledge of temporal and higher order logics, or consultation with formal methods experts. The SCR method provides a tabular notation for specifying requirements and a set of "light-weight" tools that detect several classes of errors automatically. The method also provides support for more "heavy-duty" tools, such as a model checker. To make model checking feasible, users can automatically apply one or more abstraction methods.

Heitmeyer, Constance, Kirby, James, and Labaw, Bruce. "Applying the SCR Requirements Method to a Weapons Control Panel: An Experience Report." To be presented at Formal Methods in Software Practice '98, Clearwater Beach, FL, March 4-5, 1998. PostScript, PDF

A major barrier to the use of formal methods in software practice is the difficulty software developers have understanding and applying the methods. To overcome this barrier, a requirements method called SCR (Software Cost Reduction) offers a user-friendly tabular notation to specify software requirements and a collection of easy-to-use tools that automatically detect many classes of errors in requirements specifications. This paper describes our experience in applying the SCR method and tools to a safety-critical military application---the problems encountered in translating the original contractor-produced software requirements specification into SCR and the lessons learned in applying the SCR technology to a practical system. The short time required to apply the SCR method, the serious safety violation detected, and the working system prototype produced demonstrate the utility and potential cost-effectiveness of SCR for developing safety-critical systems.

Heitmeyer, Constance. "Using the SCR* Toolset to Specify Software Requirements." Proceedings, Second IEEE Workshop on Industrial Strength Formal Specification Techniques (WIFT'98), Boca Raton, FL, Oct. 19, 1998. PostScript, PDF

Formulated in the late 1970s to specify the requirements of the Operational Flight Program (OFP) of the A-7 aircraft, the SCR (Software Cost Reduction) requirements method is a method based on tables for specifying the requirements of software systems. During the 1980s and the early 1990s, many companies, including Bell Laboratories, Grumman, Ontario Hydro, and Lockheed, applied the SCR requirements method to practical systems. Each of these applications of SCR had, at most, weak tool support. To provide powerful, robust tool support customized for the SCR method, we have developed the SCR* toolset. To provide formal underpinnings for the method, we have also developed a formal model which defines the semantics of SCR requirements specifications.

Heitmeyer, Constance L., Kirby, James Jr., Labaw, Bruce, Archer, Myla, Bharadwaj, Ramesh, "Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications," IEEE Transactions on Software Engineering, vol. 24, no. 11, November 1998. PostScript [WARNING: 10MB], PDF

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.

Heitmeyer, Constance, "SCR: A Practical Method for Requirements Specification," Proc., 17th AIAA/IEEE/SAE Digital Avionics System Conference (DASC), Bellevue, WA, Oct. 31-Nov. 7, 1998. PostScript, PDF

A controversial issue in the formal methods research community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method. A premise of this paper is that formal methods research has produced several techniques with potential utility in practical software development, but that mathematical sophistication and theorem proving skills should not be prerequisites for using these techniques. In the paper, several attributes needed to make a formal method useful in practice are described. These attributes include user-friendly notation, automated (i.e., push-button) analysis, and easy to understand feedback. To illustrate the attributes of a practical formal method, a formal method for requirements specification called SCR (Software Cost Reduction) is introduced.

Jeffords, R. and Heitmeyer, C. "Automatic Generation of State Invariants from Requirements Specifications," to be presented at 6th International Symposium on the Foundations of Software Engineering (FSE-6), Orlando FL, Nov. 3-5, 1998. PostScript, PDF

Automatic generation of state invariants, properties that hold in every reachable state of a state machine model, can be valuable in software development. Not only can such invariants be presented to system users for validation, in addition, they can be used as auxiliary assertions in proving other invariants. This paper describes an algorithm for the automatic generation of state invariants that, in contrast to most other such algorithms, which operate on programs, derives invariants from requirements specifications. Generating invariants from requirements specifications rather than programs has two advantages: 1) because requirements specifications, unlike programs, are at a high level of abstraction, generation of and analysis using such invariants is easier, and 2) using invariants to detect errors during the requirements phase is considerably more cost-effective than using invariants later in software development. To illustrate the algorithm, we use it to generate state invariants from requirements specifications of an automobile cruise control system and a simple control system for a nuclear plant. The invariants are derived from specifications expressed in the SCR (Software Cost Reduction) tabular notation.

Kang, Myong H., Moore, Andrew P. and Moskowitz, Ira S. "Design and Assurance Strategy for the NRL Pump," IEEE Computer Magazine, April 1998, vol. 31, no. 4. PostScript, PDF

The NRL Pump forwards messages from a low-level system to a high-level system and monitors the timing of acknowledgments from the high system to minimize leaks. It is the keystone to a proposed architecture that uses specialized high-assurance devices to separate data at different security levels.

Kang, Myong H., Froscher, Judith N. and Eppinger, Brian J., "Towards an Infrastructure for MLS Distributed Computing," submitted for publication at the Annual Computer Security Applications Conference, IEEE Computer Society. PostScript, PDF

Distributed computing owes its success to the development of infrastructure, middleware, and standards (e.g., CORBA) by the computing industry. This community has also recognized the need to protect information and has started to develop commercial security infrastructures and standards. The US Government must protect national security information against unauthorized information flow. To support MLS distributed computing, a MLS infrastructure must be built that enables information sharing among users at different classification levels. This infrastructure should provide MLS services for protection of classified information and use both the emerging distributed computing and commercial security infrastructures. The resulting infrastructure will enable users to integrate commercial information technology products into their systems.

In this paper, we examine the philosophy that has led to successful distributed computing among heterogeneous, autonomous components and propose an analogous approach for MLS distributed computing. We identify some services that are required to support MLS distributed computing, argue that these services are needed regardless of the MLS architecture used, present an approach for designing these services, and provide design guidance for a critical building block of the MLS infrastructure.

Kassab, Lora, and Greenwald, Steven, "Towards Formalizing the Java Security Architecture in JDK 1.2," Proceedings European Symposium on Research in Computer Security (ESORICS) '98, Springer LNCS, Leuven-la-Neuve, Belgium, September, 1998. PostScript, PDF

The Java security architecture in the Java Development Kit 1.2 expands the current Java sandbox model, allowing finer-grained, configurable access control for Java code. This new security architecture permits more precise, yet flexible, protection for both remote code (loaded across a network connection) and local code (residing on the same machine running the Java Virtual Machine) developed using the Java programming language. Our formal model and analysis is intended to: (1) allow designers and implementors to understand and correctly use the protection provided by these security controls, and (2) provide guidance to a JVM implementor wishing to support these security controls. Access control decisions in Java are made based on the current execution context using stack introspection. To model this, we employ a state-based model that uses multiple access control matrices to model the security controls in JDK 1.2. We also present a safety analysis and discuss the effects of static and dynamic security policies for a given Java Virtual Machine.

Kassab, Lora, and Voas, Jeffrey, "Agent Trustworthiness," In Proceedings of ECOOP Workshop on Distributed Object Security and 4th Workshop on Mobile Object Systems Secure Internet Mobile Computations, INRIA, Brussels, July 20-21, 1998, pp. 121-134. PostScript, PDF

Agent-based technology could revolutionize the manner by which distributed computation is performed. The fact that the information returned by an agent to the agent owner cannot be validated by the owner is impeding the widespread adoption of agent-based computing. Our paper addresses this concern by proposing a new type of software assertion to increase observability by providing agent owner's with agent state "snap-shots." These snap-shots provide agent owners with: (1) a means to determine whether its agent's results are trustworthy, (2) information to debug a roving agent, (3) a greater ability to meet real-time constraints, and (4) a means to identify hosts systems that are resource-deficient, grant insufficient access rights, or tamper with agents. We present a methodology and tool for selecting and embedding protective assertions into agent code. We also discuss how the information from the assertions is automatically analyzed. Although our proposed assertions are not foolproof, they make it much harder for an agent to be tampered with in ways that are not detectable by the agent's owner. This knowledge is paramount for the utility of an agent-based system.

Kassab, Lora, and Voas, Jeffrey, "Towards Fault-tolerant Mobile Agents," In Proceedings of Distributed Computing on the Web Workshop (DCW '98), Rostock, Germany, June, Univ. Rostock Press, 1998, pp. 96-106. PostScript, PDF

The absence of a trusted computing base for mobile agents poses serious security issues for both the host system and the survivability of the agent. Once a mobile agent is dispatched, asserting anything about the host system, the agent's behavior, or even the agent's existence is difficult to ascertain. In order to employ agents with any degree of confidence, constraints need to be placed on the agent computation since no restraints can be imposed (or assumed) about the host system's hardware or software. This paper presents a fault-tolerant approach for increasing an agent owner's confidence in the integrity of its agent.

Kruus, Peter. "A Survey of Multicast Security Issues and Architectures," 21st National Information Systems Security Conference, Arlington, VA, October 5-8, 1998. PostScript, PDF

This paper addresses issues relevant to implementing security for IP multicast networks. These issues are of importance to application developers wishing to implement security services for their multicast applications. The paper investigates the steps required to create a secure multicast session including issues of group membership and key distribution. A common simple criteria is established that can be used to evaluate multicast keying architectures. The criteria focuses on the efficiency and scalability of the keying solution. Using this criteria, several keying architectures are evaluated and compared to determine their strengths and weaknesses.

Kruus, Peter, and Macker, Joseph. "Techniques and Issues in Multicast Security," MILCOM 98, Boston, MA, October 18-21, 1998. Paper: PostScript, PDF, Presentation: PostScript, PDF

Multicast networking support is becoming an increasingly important future technology area for both commercial and military distributed and group-based applications. Integrating a multicast security solution involves numerous engineering tradeoffs. The end goal of effective operational performance and scalability over a heterogeneous internetwork is of primary interest for widescale adoption and application of such a capability. Various techniques that have been proposed to support multicast security are discussed and their relative merits are explored.

Meadows, Catherine and Paul Syverson, "A Formal Specification of Requirements for Payment Transactions in the SET Protocol," DRAFT for Preproceedings of Financial Cryptography 98, Anguilla, BWI, Feb. 23-26, 1998. PostScript Body, PostScript Figures, PDF Body, PDF Figures

Payment transactions in the SET (Secure Electronic Transaction) protocol are described. Requirements for SET are discussed and formally represented in a version of NPATRL (the NRL Protocol Analyzer Temporal Requirements Language). NPATRL is language for expressing generic requirements, heretofore applied to key distribution or key agreement protocols. Transaction vectors and other new constructs added to NPATRL for reasoning about SET payment transactions are described along with properties of their representation.

Reed, Michael G., Paul F. Syverson, and David M. Goldschlag, "Anonymous Connections and Onion Routing," IEEE Journal on Selected Areas in Communication Special Issue on Copyright and Privacy Protection, 1998. Postscript, PDF

Onion Routing is an infrastructure for private communication over a public network. It provides anonymous connections that are strongly resistant to both eavesdropping and traffic analysis. Onion routing's anonymous connections are bidirectional and near real-time, and can be used anywhere a socket connection can be used. (In some contexts not even socket connections are needed to use onion routing.) Any identifying information must be in the data stream carried over an anonymous connection. An onion is a data structure that is treated as the destination address by onion routers; thus, it is used to establish an anonymous connection. Onions themselves appear differently to each onion router as well as to network observers. The same goes for data carried over the connections they establish. Proxy aware applications, such as web browsing and email, require no modification to use onion routing, and do so through a series of proxies. A prototype of onion routing is running in our lab. This paper describes anonymous connections and their implementation using onion routing. This paper also describes several application proxies for onion routing, as well as configurations of onion routing networks.

Syverson, Paul. "Weakly Secret Bit Commitment: Applications to Lotteries and Fair Exchange", Proceedings of the 1998 IEEE Computer Security Foundations Workshop (CSFW11), Rockport Massachusetts, June 1998. Postscript, PDF

This paper presents applications for the weak protection of secrets in which weakness is not just acceptable but desirable. For one application, two versions of a lottery scheme are presented in which the result of the lottery is determined by the ticket numbers purchased, but no one can control the outcome or determine what it is until after the lottery closes. This is because the outcome is kept secret in a way that is breakable after a predictable amount of time and/or computation. Another presented application is a variant on fair exchange protocols that requires no trusted third party at all.

Back to the CHACS Publications Page.

Back to the Publications Page.