Towards a Formal Verification of a Secure and Distributed System and Its Applications
CALIFORNIA UNIV DAVIS DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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.
- Computer Programming and Software
- Computer Systems
- Computer Systems Management and Standards