Visible to the public A Language and Framework for Development of Secure Mobile Applications - January 2017Conflict Detection Enabled

Public Audience
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.

PI(s): Jonathan Aldrich (CMU), Josh Sunshine (CMU)

1) HARD PROBLEM(S) ADDRESSED (with short descriptions)
This refers to Hard Problems, released November 2012.

a. Scalability and composability is a primary concern of the project. The goal is to produce a language and framework that enables the construction of secure mobile applications with known security properties. The framework-based approach requires composition between the framework and its plugins, with modular type system and analysis techniques that avoid reanalyzing each individual component. Key issues include scalability (e.g. between client, server, and other distributed resources), tool usability, and security attributes such as confidentiality, integrity, and mitigation of common vulnerabilities seen in present technologies.

b. Human behavior is also secondarily relevant, both because human limitations are the cause of many of the security vulnerabilities that we hope to eliminate, but also because an understanding of the way humans develop software is key to ensuring that our approach is usable and enhances (rather than detracts from) developer productivity.

2) PUBLICATIONS - for Current Quarter
Report papers written as a results of this research. If accepted by or submitted to a journal, which journal. If presented at a conference, which conference.

  • Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew Hammer. Hazelnut: A Bidirectionally Typed Structure Editor Calculus. To appear in the Symposium on Principles of Programming Languages (POPL), 2017.
  • Jonathan Aldrich and Alex Potanin. Naturally Embedded DSLs. In the Workshop on Domain-Specific Language Design and Implementation (DSLDI), October, 2016.
  • Cyrus Omar and Jonathan Aldrich. Programmable Semantic Fragments. In the International Conference on Generative Programming: Concepts and Experience (GPCE), October, 2016.

3) KEY HIGHLIGHTS
Providing programmers with mechanisms for constructing commands that are as convenient as strings while being as secure as prepared SQL statements is a promising mechanism for eliminating injection vulnerabilities. Mechanisms for embedding domain-specific languages (DSLs) for constructing commands within a programming language exist, but none have achieved widespread use, in part because prior techniques were unmodular, so that separately-defined embedded DSLs could not be used together. We describe a novel mechanism called type-specific languages that supports modular DSL embeddings by associating a unique DSL with appropriate types. Our paper describing this work, entitled "Safely Composable Type-Specific Languages," was awarded an ECOOP '14 distinguished paper award.