Knight, John
Primary Appointment
Computer Science
Contact Information
Email: jck@virginia.edu
Research Interests
Software reliability and software engineering
Research Description
Echo?Practical Formal Verification
Echo is a novel yet practical approach to the formal verification of implementations. The approach splits verification into two major parts. The first part verifies an implementation against a low-level specification written using source-code annotations. The second extracts a high-level specification from the implementation with the low-level specification, and proves that it implies the original system specification from which the system was built. Semantics-preserving refactorings are applied to the implementation in both parts to reduce the complexity of the verification. Much of the approach is automated. It reduces the verification burden by distributing it over separate tools and techniques, and it addresses both functional correctness and high-level properties at separate levels.
Part of what makes Echo practical is a technique called verification refactoring in which the program to be verified is mechanically refactored. Proofs that the semantics of the refactored program are equivalent to those of the original program, that the code conforms to the annotations, and that the extracted specification implies the program?s original specification constitute the verification argument.
Helix?A Self Regenerative Architecture
The Helix self-regenerative architecture is designed to be a next generation network security architecture. Helix employs a combination of defense mechanisms that is both highly effective and metamorphic, thereby presenting attackers with a continuously changing attack surface, i.e., a metamorphic shield, that is altered routinely and as attacks progress. An attack that manages to overcome these defenses is then faced with the Helix innate response mechanism which creates a more aggressive system metamorphosis. This metamorphosis seeks to contain the effects of the attack and to reconfigure to provide rapid recovery and continued service. Finally, the Helix adaptive response mechanism examines the basic application system design at the level of its implementation and effects repairs that will ensure that future attacks of the same or similar form will be deflected, either by removing the path to vulnerabilities or the vulnerabilities themselves.
Assurance Based Development
Assurance Based Development (ABD) is the synergistic construction of a critical computing system and an assurance case that sets out the dependability claims for the system and argues that the available evidence justifies those claims. Co-developing the system and its assurance case helps software developers to make technology choices that address the specific dependability goal of each component. This approach gives developers: (1) confidence that the technologies selected will support the system?s dependability goal and (2) flexibility to deploy expensive technology, such as formal verification, only on components whose assurance needs demand it. ABD simplifies the detection?and thereby avoidance?of potential assurance difficulties as they arise, rather than after development is complete.