Automata-Based

 

home1gif.gif (1270 bytes)next1.gif (1276 bytes)     

Automata-Based Security

Formal Support for High Assurance Systems

Fred Schneider
Department of Computer Science
Cornell University
fbs@cs.cornell.edu

Project Description:

This research strives to get leverage from formal methods for solving problems that arise in practical systems settings.

Reasoning about real-time programs in environments. We will develop formal logics for reasoning about programs whose execution is constrained by scheduling algorithms, resource bounds, and physical quantities that change over time. The logics will be proved sound and complete. Their utility will be evaluated by proving non-trivial system examples. At a minimum, the examples will include FCFS, priority, and priority-inheritance schedulers, processor and bus contention, and some process control problems.

Methodology for Fault-tolerant Services. We will develop a verification framework that is specialized to fault tolerance. This approach permits more-natural specifications of fault-tolerance requirements than general-purpose formalisms and supports mechanized analysis of system fault-tolerance. A prototype analysis tool will embody the approach in order to understand its limitations and motivate useful extensions.

Accomplishments:

Our work on equational propositional and first-order logics is summarized in the following publications.

A Logical Approach to Discrete Math. Springer Verlag, NY, 1993, 500 pages. With David Gries.
Instructor's Manual for "A Logical Approach to Discrete Math". Ithaca, 1993. 311 pages. With David Gries.
Equational propositional logic. Information Processing Letters 53,3 (February 1995), 145-152. With David Gries.
A new approach to discrete teaching mathematics. Primus V,2 (June 1995), 113-138. WIth David Gries.
Teaching math more effectively, through the design of calculational proofs. The Mathematical Monthly (October 1995), 691-697. With D. Gries.
Avoiding the undefined by underspecification. Computer Science Today Recent Trends and Developments (Jan van Leeuwen, ed).
Lecture Notes in Computer Science, Vol. 1000, Spring-Verlag, 1995, 366-373. With David Gries.

Our work on reasoning about programs is summarized in the following publications.

A formalization of priority inversion. Real Time Systems 5, (1993), 285-303. With Ozalp Babaoglu and Keith Marzullo.
Proving nondeterministically specified safety properties using progress measures. Information and Computation 107,3 (November 1993), 151-170. With N. Klarlund.
Reasoning about programs by exploiting the environment. Proc. 21st International Colloquium, ICALP'94 (Jerusalem, Israel, July 1994), Lecture Notes in Computer Science, Volume 820, Springer-Verlag, New York, 328-339. With Limor Fix.
Hybrid verification by exploiting the environment. Formal Techniques in Real Time and Fault Tolerant Systems (Lubeck, Germany, September 1994), Lecture Notes in Computer Science, Volume 863, Springer-Verlag, New York, 1-18. With Limor Fix.
Refinement for fault-tolerance: An aircraft hand-off protocol. Foundations of Ultradependable Parallel and Distributed Computing, Paradigms for Dependable Applications, Kluwer Academic Publishers, 1994, 39-54. With Keith Marzullo and Jon Dehn.

Our work on mobile agents and the TACOMA project is summarized in the following publications. See also the TACOMA web page.

Operating system support for mobile agents. Proc. Fifth Workshop on Hot Topics in Operating Systems HOTOS-V (Orcas Island, Washington, May 1995), 42-45. With Dag Johansen and Robbert van Renesse.
Supporting Broad Internet Access to TACOMA. To appear, Proc. Seventh ACM SIGOPS European Workshop (September 1996). With Dag Johansen and Robbert van Renesse.
Cryptographic Support for Fault-Tolerant Computing To appear, Proc. Seventh ACM SIGOPS European Workshop (September 1996). With Yaron Minsky, Robbert van Renesse, and Scott D. Stoller.

Our work on implementing fault-tolerant and distributed systems is summarized in the following publications.

Faster possibility detection by combining two approaches. Proc. 9th International Workshop, WDAG '95, (Le Mont-Saint- Michel, France, Sept. 1995). Lecture Notes in Computer Science, Vol. 972, Springer-Verlag, New York, 1995, 318-332. With Scott D. Stoller.
Avoiding AAS Mistakes. Proceedings of the Air Traffic Management Workshop (eds. L. Tobais, M. Tashker, A. Boyle). NASA Conference Publication 10151, NASA Ames Research Center, 133-149.
Hypervisor-based Fault Tolerance. Proceedings of the Fifteenth ACM Symposium on Operating Systems Principles, Operating Systems Review 29, 5 (Copper Mountain Resort, Colorado, Dec. 1995), 1-11. With T. Bressoud.
Hypervisor-based Fault Tolerance. ACM Transactions on Computer Systems 14, 1 (Feb. 1996), 80-107. With T. Bressoud.