SoS Quarterly Summary Report - CMU - April 2017

Lablet Summary Report -- Highlights from the CMU Projects

A). Fundamental Research
High level report of result or partial result that helped move security science forward-- In most cases it should point to a "hard problem".

Theoretical studies

Secure composition of systems and policies (Datta, Jia, Chaki [SEI], Maniatis [Google])

The UberSpark system, developed within this project, enforces high-level abstractions (e.g., secure objects, interface rules, access control, some concurrency rules, etc.) in the context of low-level systems software, specifically C99 and assembly code, where such protections normally do not exist. The absence of such protections is an important source of binary-level security vulnerabilities. The UberSpark system includes a verified assembly language, CASM, whose programs can be compiled using the certifying CompCert compiler into executables. Performance impact of the use of UberSpark and its verification of security-related invariants was tested and was very minor. The developing system is available at http://uberspark.org. A complementary capability, System M, allows proofs of safety for programs that execute adversary-supplied code without forcing the adversarial code to be available for deep typing analysis.

Empirical studies

Design and Composition of Security and Privacy Policies (Breaux, Niu [UTSA])

Regulatory requirements regarding published privacy policies create demand for effective techniques to assure that mobile applications, for example, are consistent with their stated policies, and this, in turn, creates a requirement that policies are able to be modeled formally to support the necessary formal reasoning. This project thus addresses the two Hard Problems of policy (modeling of policies), metrics (assessment of compliance of policy and implementation), and human behavior (policy comprehension). There are recent results focused on the challenge of formal modeling of policies, with results signaling the potential for automated support in developing formal policy models. There are also results that demonstrate the extent of privacy policy violations in a survey of top Android apps (63 violations for 501 apps).

User Security Behavior (Acquisti, Cranor, Christin, Telang, Egelman [Berkeley], Beach [Pitt])

Work on larger-scale studies in the Security Behavior Observatory continues, with a focus primarily on the Hard Problem of human behavior (end user security-related behavior). Here is one highlight result: In between-subjects experiments (661 participants), the use of "fingerprint" representations of cryptographic keys by humans (e.g., as a proxy for a public key) was assessed. Depending on how fingerprints were presented, attacks succeeded between 6% and 72% of the time. Compare-and-select methods, while intuitive and fast, performed poorly. A conclusion is that

Secure systems development

A Language and Framework for Development of Secure Mobile Applications (Aldrich, Sunshine)

Embedded domain specific languages (DSLs) create vulnerabilities, with SQL injection as the most notable example. This project develops a principled approach, called type specific languages, to embedding of DSLs in larger systems. This technology addresses specifically the Hard Problems of composability (of multiple DSLs within larger systems) and human behavior (to help systems developers develop secure code at the outset of a project). In the recent quarter, two publications appeared, one in the high selective POPL conference and the other in a POPL workshop, that applied these ideas to the development of structure editors to facilitate software development, but in a manner that is both type safe and easily usable by developers at all levels of capability.

Science of secure frameworks (Garlan, Aldrich, Sunshine, Schmerl, Abi Antoun [Wayne State], Malek [UCI])

The Android framework and ecosystem are an example of very wide-scale adoption of a framework-based architecture. This project addresses the Hard Problems of composition (frameworks and static assurance of security properties) and resilience (design and tooling to support resiliency in practice). The team developed a system for determining and enforcing least-privilege architecture for Android, called DELDROID. The system uses static analysis to identify the least-privilege level actually needed, so this can be enforced at runtime - reducing security risks.

B). Community Interaction
Work to explain or extend scientific rigor in the community/culture. Workshops, Seminars, Competitions, etc.

The UberSpark prototype is now open-sourced and available on the web (http://uberspark.org)
The Garlan/Schmerl project on multi-model runtime security analysis is now working directly with an internal NSA group.

C. Educational
Any changes to curriculum at your school or elsewhere that indicates an increased training or rigor in security research.

Nothing to report this quarter