Assured Android Execution Environments
Abstract
The goal of this research is to determine methods of assuring isolation when executing Android software in a contained environment. A three-stage methodology called The Formal Verification Cycle is presented. This cycle focuses on the iteration over a set of security properties to validate each within a specification and their verification within a software implementation. A security property can be validated when its functional language prototype (e.g. a Haskell coded version of the property) is converted and processed by a formal method (e.g. a theorem proof assistant). This validation of the property enables the definition of the property in a software specification, which can be implemented separately in an imperative programming language (e.g. the Go programming language). Once the implementation is complete another formal method can be used (e.g symbolic execution) to verify the imperative implementation satisfies the validated specification. Successful completion of this cycle shows a given implementation is equivalent to a functional language prototype, and this cycle assures a specification for the original desired security properties was properly implemented.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 23, 2018
- Accession Number
- AD1056149
Entities
People
- Brandon P Froberg
Organizations
- Air Force Institute of Technology