Research
From Dependability
Contents |
Helix Self-Regenerative Architecture
The band-aid approach to protecting information systems via patching is widely considered to be inadequate. Even approaches that incorporate intrusion detection and tolerance have proven ineffective against determined and well-funded attackers who have at their disposal a growing arsenal of evasive, stealthy, adaptive, polymorphic and metamorphic attacks. A fundamental problem with current defenses is that they do not redress the asymmetry between attackers and defenders, changing the target system only slowly and reactively in response to attacks.
The Helix self-regenerative architecture, on the other hand, begins with 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.
Software Dynamic Translation
A fundamental problem with current defenses is that they do not redress the asymmetry between attackers and defenders, changing the target system only slowly and reactively in response to attacks. The Helix self-regenerative architecture begins with a combination of defense mechanisms that is both highly effective and metamorphic, thereby presenting attackers with a continuously changing attack surface 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.
Strata
Software dynamic translation (SDT) is a technology that permits the modification of an executing program's instructions. In recent years, SDT has received increased attention, from both industry and academia, as a feasible and effective approach to solving a variety of significant problems. Despite this increased attention, the task of initiating a new project in software dynamic translation remains a difficult one. To address this concern, and in particular, to promote the adoption of SDT technology into an even wider range of applications, we have implemented Strata, a cross-platform infrastructure for building software dynamic translators.
Security
Web Application Security
The PHPrevent project seeks to provide a fully automated and user-friendly approach to securely hardening web applications from SQL injection, script injection and cross-site scripting attacks.
Genesis: Security through Diversity
The Genesis project seeks to reproduce the genetic diversity found in nature by deliberately and systematically introducing diversity in software components. The hope is that while the phenotype of software components will be similar (its functional behavior), its genotype will contain enough variations to protect the population against a broad class of diseases (attacks, aging).
N-Variant Systems Framework
The N-Variant Systems Framework is a new approach to software service protection that is based on software system structures which combine monitoring software and tailored program diversity. The resulting systems have two valuable properties that cannot be achieved with previous vulnerability-masking approaches: (1) their effectiveness does not depend on keeping secrets from adversaries; and (2) we can construct proofs that a system cannot be compromised by a class of attacks, no matter what vulnerabilities exist in the server program.
Software Memory Protection
The Software Memory Protection project seeks to defend programs against memory overwriting attacks by developing general defenses for the prevention, detection, and remediation of a large variety of memory overwriting attacks. In contrast to prior work, the techniques are equally applicable to the protection of critical data in global, heap, or stack data regions. Furthermore, access to program source code and dependence on particular compilers are avoided by operating directly on program binaries. This is accomplished by the use of static binary analysis and rewriting tools in combination with the Strata portable software dynamic translation framework.
Formal and Natural Languages in Software Systems
The CLEAR Method
Miscommunication of software requirements has been implicated in a disproportionate number of faults and failures in safety-critical and other systems, as well as in schedule and cost overruns that further burden resources. Drawing from cognitive psychology, the CLEAR Method (Cognitive Linguistic Elicitation And Representation), is a methodology for eliciting and representing software requirements in a structured form to eliminate or prevent sources of critical miscommunication.
ECHO
Safe operation is crucial to safety-critical systems, and formal verification of implementations is a desirable means to increase confidence in safety. Traditional formal verification approaches follow the Floyd-Hoare style, setting up a direct compliance argument between an abstract formal specification and a concrete implementation. Such approaches require proofs of large numbers of verification conditions. Creation of both the conditions and their proofs can be difficult and time-consuming. We introduce a general formal verification approach that closely models the Floyd-Hoare pattern, yet avoids the tedious direct compliance proof between the formal specification and the implementation. The approach moves the major proof step to a point between two abstract specifications.
Situated Formalisms
When developing any formalism for a software system, from an abstract formal specification to a source code implementation, developers focus on the formal properties of what they build. These formal properties, however, are not able to convey an intuition of how the software should perform in its intended environment. Developers often include notes to themselves in the form of "meaningful" variable names or source code comments, but this is ad hoc and insufficient when building safety-critical computing systems. We are working to develop a structure for formalisms that includes natural language content to situate them in terms of their operating environment.
Zeus Toolkit
Our goal is to understand the relative lack of use of formal techniques in commercial software development. To validate our hypothesis that one of the reasons for this lack of use is the lack of support tools, we have developed an extension to Adobe FrameMaker to support specification development using the formal language Z.
Survivable Systems
The Willow Survivability Control Architecture
Willow is a general survivability control architecture for large-scale distributed information systems. Based on Willow we have developed applications such as:
- Autonomic network defenses against cyber-attacks such as worms and viruses
- STILT, a System for Terrorism Intervention and Large-scale Teamwork
- Supporting dependability and survivability attributes in large-scale grid systems
STILT
Based on Willow, STILT, the System for Terrorism Intervention and Large-scale Teamwork, is a Command and Control systems for emergency response and homeland security.
Survivable Safety-Critical Systems
Software is a human work product. As such there is no way to guarantee that it will not contain design flaws. These flaws are much less likely to exist, however, if software is smaller or simpler and thus easier for its designers to comprehend. We are working on transitioning survivability, a concept from the domain of networked systems, to the domain of safety-critical systems.
Dependable Grids
Large-scale distributed systems, or grids, are becoming interwoven within the fabric of society. As our reliance on grids grows considerably over time, they will become critical infrastructure. Our research goal is to enable the engineering of dependable grids; grids that provide services on which we can justifiably place our trust.
Safety Analysis
Safety Cases
Safety cases provide a structured methodology for reasoning about the safety of systems. By explicitly connecting the safety goals the developer must satisfy to evidence that they have been met, safety cases present more compelling arguments that a system is safe than do the ad hoc and process-based approaches in widespread use today. We are developing a framework, the enhanced safety case lifecycle for incorporating safety cases within the software lifecycle.
Software Forensics
Incidents and accidents that can be attributed to software failure often result in tragedies and other losses. The need to learn from these events grows more critical as software systems become more complex and the ways they can fail become less intuitive. Clear access to retrospective information about the complex and systemic causes of incidents and accidents is not provided by existing software development methods, and what is known from forensic engineering generally as well as the study of failure have yet to be applied comprehensively to software. Forensic software engineering, or software forensics, refers to the body of work aimed at addressing these deficiencies.
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.
Dependability Reading Group
A reading group that focuses on topics related to dependability and safety analysis. The Reading Group is a group of students and faculty interested in discussing security related topics. Anyone is welcome to attend the meetings. The group usually meets on Wed. 12:00-1:00pm and may move it to other times depending on talks or other conflicts within the department.