Specifying and Checking Security Properties in an Evolving Software Base
Abstract
Research funded under this grant led to the development of techniques and tools for protecting privacy in a decentralized environment and achieving Byzantine Fault Tolerance (BFT), and a methodology that enables BFT replicas to run different implementations. The work led to an innovative new security model that allows static checking of security properties, a new annotation language for expressing security properties, extensions to Java that allow code to use the new model, lightweight tools for checking security properties of both source code (via a new compiler) and byte codes (via a new bytecode verifier), and a study of runtime support needed by the model. A new replications algorithm (BFT) that is robust against Byzantine failures was developed. It is efficient, works in an asynchronous environment and can be used to harden critical system services. An extension to BFT, called BFT with Abstract Specification Encapsulation (BASE), was developed to allow different software to run at different replicas so as to avoid failures due to software bugs. It provides a way of achieving practical N-version programming in which different versions are developed by different organizations and also the different versions may differ in the details of their behavior, i.e., support slightly different specifications.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 2003
- Accession Number
- ADA417672
Entities
People
- Barbara H. Liskov
Organizations
- Massachusetts Institute of Technology