| Increased Information Flow Needs for High-Assurance Composite Evaluations |
|
| High Confidence Software and Systems: A Rockwell Collins Perspective |
|
| Theorem Provers as High Assurance Programming Environments |
|
| Usage of Intermediate Java Byte Code to Verify Wireless Java Applications |
|
| Formally Verified Encryption of High-Level Datatypes: An Application of Polytypism |
|
| Transparency: An Application Context for High Confidence Software and Systems (HCSS) Tools and Methods |
|
| Modelling Key Distribution, Art to Science |
|
| Security by Construction - Engineering Software to Exceed EAL5 |
|
| Synthesis of Provably Correct Java Card Applets and Platform |
|
| Designing and Testing a High Assurance ASN.1 Compiler |
|
| Organically Assured and Survivable Information Systems |
|
| Code Generation for High-Assurance Java Card Applets |
|
| vFaat: von Neumann Formal Analysis and Annotation Tool |
|
| Cryptyc: A Cryptographic Protocol Typechecker |
|
| Programatica Tools for Certifiable, Auditable Development of High Assurance Systems in Haskell |
|
| Trustworthy Refinement through Intrusion-Aware Design (TRIAD) |
|
| Overview FAA IT & ISS R&D: Security Today Security Tomorrow |
|
| Secure Software from Design to Binary |
|
| Large Scale Separation Through Monads: The Oregon Separation Kernel |
|
| Cryptol: A Domain Specific Language for Cryptography |
|
| GemClassifier, a Formally Developed Smart Card |
|
| Compositional Assurance for MILS |
|
| Verifying a High-Performance Micro-kernel |
|
| ARM Verification |
|
| Circuit Specification, Abstraction, and Reverse Engineering |
|