Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Keyword
-
- Android (2)
- Formal verification (2)
- Access control (1)
- Autocorres (1)
- Boot loading (1)
-
- C++ (1)
- Computer security (1)
- Heap allocator (1)
- Isabelle (1)
- Isolation (1)
- Language-based techniques (1)
- Oblivious memory (1)
- Operating system (1)
- Privacy (1)
- Refinement (1)
- Security (1)
- Side-channel attacks (1)
- Smartphone (1)
- Systems programming (1)
- TPM chip (1)
- Trusted computing (1)
- Virtualization (1)
Articles 1 - 5 of 5
Full-Text Articles in Physical Sciences and Mathematics
Liboblivious: A C++ Library For Oblivious Data Structures And Algorithms, Scott D. Constable, Steve Chapin
Liboblivious: A C++ Library For Oblivious Data Structures And Algorithms, Scott D. Constable, Steve Chapin
Electrical Engineering and Computer Science - Technical Reports
Infrastructure as a service (IaaS) is an enormously beneficial model for centralized data computation and storage. Yet, existing network-layer and hardware-layer security protections do not address a broad category of vulnerabilities known as side-channel attacks. Over the past several years, numerous techniques have been proposed at all layers of the software/hardware stack to prevent the inadvertent leakage of sensitive data. This report discusses a new technique which integrates seamlessly with C++ programs. We introduce a library, libOblivious, which provides thin wrappers around existing C++ standard template library classes, endowing them with the property of memory-trace obliviousness.
Formal Verification Of A Modern Boot Loader, Scott D. Constable, Rob Sutton, Arash Sahebolamri, Steve Chapin
Formal Verification Of A Modern Boot Loader, Scott D. Constable, Rob Sutton, Arash Sahebolamri, Steve Chapin
Electrical Engineering and Computer Science - Technical Reports
We introduce the Syracuse Assured Boot Loader Executive (SABLE), a trustworthy secure loader. A trusted boot loader performs a cryptographic measurement (hash) of program code and executes it unconditionally, allowing later-stage software to verify the integrity of the system through local or remote attestation. A secure loader differs from a trusted loader in that it executes subsequent code only if measurements of that code match known-good values. We have applied a rigorous formal verification technique recently demonstrated in practice by NICTA in their verification of the seL4 microkernel. We summarize our design philosophy from a high level and present our …
A Formally Verified Heap Allocator, Arash Sahebolamri, Scott D. Constable, Steve J. Chapin
A Formally Verified Heap Allocator, Arash Sahebolamri, Scott D. Constable, Steve J. Chapin
Electrical Engineering and Computer Science - Technical Reports
We present the formal verification of a heap allocator written in C. We use the Isabelle/HOL proof assistant to formally verify the correctness of the heap allocator at the source code level. The C source code of the heap allocator is imported into Isabelle/HOL using CParser and AutoCorres. In addition to providing the guarantee that the heap allocator is free of bugs and therefore is suitable for use in security critical projects, our work facilitates verification of other projects written in C that utilize Isabelle and AutoCorres.
Pinpoint: Efficient And Effective Resource Isolation For Mobile Security And Privacy, Paul Ratazzi, Ashok Bommisetti, Nian Ji, Wenliang Du
Pinpoint: Efficient And Effective Resource Isolation For Mobile Security And Privacy, Paul Ratazzi, Ashok Bommisetti, Nian Ji, Wenliang Du
Electrical Engineering and Computer Science - All Scholarship
Virtualization is frequently used to isolate untrusted processes and control their access to sensitive resources. However, isolation usually carries a price in terms of less resource sharing and reduced inter-process communication. In an open architecture such as Android, this price and its impact on performance, usability, and transparency must be carefully considered. Although previous efforts in developing general-purpose isolation solutions have shown that some of these negative sideeffects can be mitigated, doing so involves overcoming significant design challenges by incorporating numerous additional platform complexities not directly related to improved security. Thus, the general purpose solutions become inefficient and burdensome if …
A Systematic Security Evaluation Of Android’S Multi-User Framework, Edward Paul Ratazzi, Yousra Aafer, Amit Ahlawat, Hao Hao, Yifei Wang, Wenliang Du
A Systematic Security Evaluation Of Android’S Multi-User Framework, Edward Paul Ratazzi, Yousra Aafer, Amit Ahlawat, Hao Hao, Yifei Wang, Wenliang Du
Electrical Engineering and Computer Science - All Scholarship
Like many desktop operating systems in the 1990s, Android is now in the process of including support for multiuser scenarios. Because these scenarios introduce new threats to the system, we should have an understanding of how well the system design addresses them. Since the security implications of multi-user support are truly pervasive, we developed a systematic approach to studying the system and identifying problems. Unlike other approaches that focus on specific attacks or threat models, ours systematically identifies critical places where access controls are not present or do not properly identify the subject and object of a decision. Finding these …