Towards a Formal Verification of a Secure and Distributed System and Its Applications

Abstract

This paper presents research towards the formal specification and verification of a secure distributed system and secure application programs that run on it. We refer to the whole system from hardware to application programs written in a concurrent programming language as the Silo and to a simplified view of the Silo as the minisilo. Both minisilo and Silo consist of a collection of microprocessors interconnected by a network a distributed operating, system and a compiler for a distributed programming language. Our goal is to verify the full Silo by mechanized layered formal proof using the higher order logic theorem proving system HOL. This paper describes our current results for verifying the minisilo and our incremental approach for evolving the verification of the minisilo into the verification of the full Silo. Scalability is addressed in part - extending, the distributed operating, system with additional server which in turn provide services that extend the programming language.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1994
Accession Number
ADA445719

Entities

People

  • Cui Zhang
  • Gregory D. Benson
  • Karl Levitt
  • Mark R. Heckman
  • Myla Archer
  • Rob Shaw
  • Ronald A. Olsson

Organizations

  • University of California, Davis

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Compilers
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Instruction Set Architecture
  • Instructions
  • Kernels (Operating System)
  • Language
  • Layers
  • Mesh Networks
  • Models
  • National Security
  • Operating Systems
  • Programming Languages
  • Security

Fields of Study

  • Computer science
  • Engineering

Readers

  • Aerospace Test and Evaluation
  • Parallel and Distributed Computing.
  • Software Engineering.