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

Submitted by Jamie Presken on Thu, 12/10/2015 - 10:27am

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
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.

  • Zack Coker, Michael Maass, Tianyuan Ding, Claire Le Goues, and Joshua Sunshine. Evaluating the Flexibility of the Java Sandbox. In Annual Computer Security Applications Conference (ACSAC), 2015.
  • Du Li, Alex Potanin, and Jonathan Aldrich. Delegation vs Inheritance for Typestate Analysis. In Workshop on Formal Techniques for Java-like Programs (FTfJP), 2015.
  • Joseph Lee, Jonathan Aldrich, Troy Shaw, and Alex Potanin. A Theory of Tagged Objects. In European Conference on Object-Oriented Programming (ECOOP), 2015.
  • Joshua Sunshine, James D. Herbsleb, and Jonathan Aldrich. Searching the State Space: A Qualitative Study of API Protocol Usability. In the International Conference on Program Comprehension (ICPC), 2015
  • Cyrus Omar, Chenglong Wang, and Jonathan Aldrich. Composable and Hygienic Typed Syntax Macros. In Symposium on Applied Computing (SAC), 2015.
  • Nathan Fulton, Cyrus Omar, and Jonathan Aldrich. Statically Typed String Sanitation Inside a Python. In Workshop on Privacy and Security in Programming (PSP), 2014. [Best Student Paper Award]
  • Darya Kurilova, Alex Potanin, and Jonathan Aldrich. Wyvern: Impacting Software Security via Programming Language Design. In Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU), 2014.
  • Michael Coblenz, Jonathan Aldrich, Brad Myers, and Joshua Sunshine. Considering Productivity Effects of Explicit Type Declarations. In Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU), 2014.
  • Cyrus Omar, Darya Kurilova, Ligia Nistor, Benjamin Chung, Alex Potanin, and Jonathan Aldrich. Safely Composable Type-Specific Languages. In European Conference on Object-Oriented Programming (ECOOP), 2014. [Distinguished Paper Award]
  • Joshua Sunshine, James D. Herbsleb, and Jonathan Aldrich. Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming. In European Conference on Object-Oriented Programming (ECOOP), 2014.
  • Michael Maass, Bill Scherlis, and Jonathan Aldrich. In-Nimbo Sandboxing. In Symposium and Bootcamp on the Science of Security (HotSOS), 2014.
  • Jonathan Aldrich. The Power of Interoperability: Why Objects Are Inevitable. In Onward! Essays, 2013.
  • Cyrus Omar, Benjamin Chung, Darya Kurilova, Alex Potanin, and Jonathan Aldrich. Type-Directed, Whitespace-Delimited Parsing for Embedded DSLs. In Workshop on the Globalization of Domain Specific Languages (GlobalDSL), 2013.
  • Ligia Nistor, Darya Kurilova, Stephanie Balzer, Benjamin Chung, Alex Potanin, and Jonathan Aldrich. Wyvern: A Simple, Typed, and Pure Object-Oriented Language. In Workshop on Mechanisms for Specialization, Generalization, and Inheritance (MASPEGHI), 2013.
  • Blase Ur, Patrick Gage Kelley, Saranga Komanduri, Joel Lee, Michael Maass, Michelle Mazurek, Timothy Passaro, Richard Shay, Timothy Vidas, Lujo Bauer, Nicolas Christin, and Lorrie Faith Cranor. How Does Your Password Measure Up? The Effect of Strength Meters on Password Creation. In USENIX Security Symposium. (Revised version to appear in the "USENIX;login:" magazine)
  • Simin Chen. Declarative Access Policies based on Objects, Relationships, and States. In SPLASH 2012 Student Research Competition.
  • Nathan Fulton. Domain Specific Security through Extensible Type Systems. In SPLASH 2012 Student Research Competition.

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.

Groups: