Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
- Publication
- Publication Type
Articles 1 - 7 of 7
Full-Text Articles in Physical Sciences and Mathematics
Formalizing Stack Safety As A Security Property, Sean Noble Anderson, Roberto Blanco, Leonidas Lampropoulos, Benjamin C. Pierce, Andrew Tolmach
Formalizing Stack Safety As A Security Property, Sean Noble Anderson, Roberto Blanco, Leonidas Lampropoulos, Benjamin C. Pierce, Andrew Tolmach
Computer Science Faculty Publications and Presentations
The term stack safety is used to describe a variety of compiler, runtime, and hardware mechanisms for protecting stack memory. Unlike “the heap,” the ISA-level stack does not correspond to a single high-level language concept: different compilers use it in different ways to support procedural and functional abstraction mechanisms from a wide range of languages. This protean nature makes it difficult to nail down what it means to correctly enforce stack safety.
Information Security Maturity Model For Healthcare Organizations In The United States, Bridget Joan Barnes Page
Information Security Maturity Model For Healthcare Organizations In The United States, Bridget Joan Barnes Page
Dissertations and Theses
This research provides a maturity model for information security for healthcare organizations in the United States. Healthcare organizations are faced with increasing threats to the security of their information systems. The maturity model identifies specific performance metrics, with relative importance measures, that can be used to enhance information security at healthcare organizations allowing them to focus scarce resources on mitigating the most important information security threat vectors. This generalizable, hierarchical decision model uses both qualitative and quantitative metrics based on objective goals. This model may be used as a baseline by which to measure individual organizational performance, to measure performance …
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise, Guglielmo Fachini, CăTăLin Hriţcu, Marco Stronati, Arthur Azevedo De Amorim, Carmine Abate, Roberto Blanco, Théo Laurent, Benjamin C. Pierce, Andrew Tolmach
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise, Guglielmo Fachini, CăTăLin Hriţcu, Marco Stronati, Arthur Azevedo De Amorim, Carmine Abate, Roberto Blanco, Théo Laurent, Benjamin C. Pierce, Andrew Tolmach
Computer Science Faculty Publications and Presentations
We propose a new formal criterion for secure compilation, giving strong end-to-end security guarantees for software components written in unsafe, low-level languages with C-style undefined behavior. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components running with least privilege. Each component is protected from all the others—in particular, from components that have encountered undefined behavior and become compromised. Each component receives secure compilation guarantees up to the point when it becomes compromised, after which an attacker can take complete control over the component and use any of its privileges to attack the remaining …
Tweakable Ciphers: Constructions And Applications, Robert Seth Terashima
Tweakable Ciphers: Constructions And Applications, Robert Seth Terashima
Dissertations and Theses
Tweakable ciphers are a building block used to construct a variety of cryptographic algorithms. Typically, one proves (via a reduction) that a tweakable-cipher-based algorithm is about as secure as the underlying tweakable cipher. Hence improving the security or performance of tweakable ciphers immediately provides corresponding benefits to the wide array of cryptographic algorithms that employ them. We introduce new tweakable ciphers, some of which have better security and others of which have better performance than previous designs. Moreover, we demonstrate that tweakable ciphers can be used directly (as opposed to as a building block) to provide authenticated encryption with associated …
Micro-Policies: Formally Verified, Tag-Based Security Monitors, Arthur Azevedo De Amorim, Maxime Denes, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach
Micro-Policies: Formally Verified, Tag-Based Security Monitors, Arthur Azevedo De Amorim, Maxime Denes, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach
Computer Science Faculty Publications and Presentations
Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies (or micro-policies) to be expressed using rules on metadata tags. We propose a methodology for defining and reasoning about such tag-based reference monitors in terms of a high-level “symbolic machine,” and we use this methodology to define and formally verify micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety; in addition, we show how to use the tagging mechanism to protect its own integrity. For each micro-policy, we prove by refinement that the symbolic machine instantiated with the policy’s rules embodies a high-level …
The Cracker Patch Choice: An Analysis Of Post Hoc Security Techniques, Crispin Cowan, Heather Hinton, Calton Pu, Jonathan Walpole
The Cracker Patch Choice: An Analysis Of Post Hoc Security Techniques, Crispin Cowan, Heather Hinton, Calton Pu, Jonathan Walpole
Computer Science Faculty Publications and Presentations
It has long been known that security is easiest to achieve when it is designed in from the start. Unfortunately, it has also become evident that systems built with security as a priority are rarely selected for wide spread deployment, because most consumers choose features, convenience, and performance over security. Thus security officers are often denied the option of choosing a truly secure solution, and instead must choose among a variety of post hoc security adaptations. We classify security enhancing methods, and compare and contrast these methods in terms of their effectiveness vs. cost of deployment. Our analysis provides practitioners …
A Policy-Independent Secure X Server, Kirk Joseph Bittler
A Policy-Independent Secure X Server, Kirk Joseph Bittler
Dissertations and Theses
This thesis demonstrates that a secure X system can be designed and implemented to be independent of a particular security policy. The advantages and costs of a separation of security policy and enforcement are examined by developing a large scale application, the DX windowing system, on a DTOS platform. DTOS is a high assurance operating system that isolates policy decisions in a Security Server. A security conscious process, such as DX, eliminates policy considerations from the code. The process instead consults the Security Server and enforces the decisions that server derives from the policy. The DX architecture is described and …