SoS Quarterly Summary Report - CMU - October 2016

Lablet Summary Report -- Highlights from the CMU Projects

A). Fundamental Research

Theoretical Foundations - these highlights extend existing methods for modeling that could not previously address the hard security problems.

• Secure composition of systems and policies (Datta, Jia). In the current quarter, we have open-sourced and released the first academic prototype of UberSpark. The artifacts and associated papers are available at: http://uberspark.org. We continue to collaborate with Google to apply UberSpark to other application domains (apart from hypervisors) to showcase the broad applicability of our framework. We have identified two application areas: password hashing and secure cloud-based web services for this purpose. Staying true to the UberSpark methodology, we are presently focusing on application and crypto properties which can be formulated as invariants directly expressible on the source-code of uObjects with associated hardware assumptions (see Fiscal Year to Date: UberSpark). More specifically,we are leveraging recent commodity hardware support for isolation, attestation and crypto (Intel Software Guard Extensions (SGX) and AES NI) while focusing on security invariants which capture foundational properties such as memory safety and error correctness as well as mathematical and functional properties. We are refining our existing high-level proofs to focus on a more general secure object abstraction with commodity hardware assumptions such as SGX, to encompass the aforementioned application domains and properties. At the same time, we are also laying the foundation for mechanization of our high-level proofs
  .
• Security Reasoning for Distributed Systems with Uncertainty (Platzer, Kozen (Cornell)). This quarter we continued work on approximating complementarity problems and variational inequalities. Variational inequalities (VI) are ubiquitous in optimization, planning, game theory, engineering and other fields. Our research looks at approximating VIs related to constrained optimization problems, where we need to think about the effect that approximation has on both the space of solution variables and the space of constraints. One important application of our research is policy synthesis for large systems with uncertainty modeled by Markov decision processes (MDPs). For MDPs the solution is a value function, and the constraints are related to the flow of probabilities through the MDP's dynamics. Optimal policies can be read off of either the flow or value functions easily. Approximating the value domain without approximating the flow domain leads to poor performance: the approximation may remove the ability to express the true solution, but we are still insisting that the value function satisfies every MDP constraint. On the other hand, approximating the constraints allows the approximate solution to violate some important aspects of the problem. What we want are approximations of the value and flow that are balanced: we weaken constraints roughly at the same rate that we weaken the capacity to represent value functions. Traditional methods for handling this problem in approximate MDP solving tends to rely on constraint sampling---only satisfying a random subset of constraints. But our initial experiments into this question indicate that this may not be the best thing to do. We are currently investigating methods for approximating the flow basis using other basis functions (like Voronoi tessellations), and balanced methods for refining the value and flow bases in response to residuals and errors in the approximate solution.

New Approaches to Security Problems - these highlights focus on new methods to address existing security problems

• A Language and Framework for Development of Secure Mobile Applications. (Aldrich, Sunshine). We developed typy, a statically typed programming language embedded by reflection into Python. Rather than defining a monolithic semantics, typy features a fragmentary semantics, i.e., it delegates semantic control over each term, drawn from Python's fixed syntax, to a contextually relevant user-defined semantic fragment. This fragment programmatically (1) typechecks the term, and (2) assigns dynamic meaning to the term by computing its translation to Python. We argue that this design is expressive with examples of fragments that express the static and dynamic semantics of (1) functional records; (2) a variation on JavaScript's prototypal object system; (3) labeled sums (with nested pattern matching a la ML); and (4) typed foreign interfaces to Python and OpenCL. These semantic structures are, or would need to be, defined primitively in other languages. We further argue that this design is compositionally well-behaved. It sidesteps the problems of grammar composition and the expression problem by allowing different fragments to deterministically share a fixed syntax. Moreover, programs are semantically stable under fragment composition. A paper describing this topic will appear in the Internationl Conference on Generative Programming: Concepts and Experiences (GPCE), 2016. Structure editors allow programmers to edit the tree structure of a program directly. This can have cognitive benefits, particularly for novice and end-user programmers (as evidenced by the popularity of structure editors like Scratch.) It also simplifies matters for tool designers, because they do not need to contend with malformed program text. We define Hazelnut, a structure editor based on a small bidirectionally typed lambda calculus extended with holes and a cursor (ala Huet's zipper.) Hazelnut goes one step beyond syntactic well-formedness: it's edit actions operate over statically meaningful (i.e., well-typed) terms. Naively, this prohibition on ill-typed edit states would force the programmer to construct terms in a rigid "outside-in" manner. To avoid this problem, the action semantics automatically places terms assigned a type that is inconsistent with the expected type inside a hole. This safely defers the type consistency check until the term inside the hole is finished. Hazelnut is a foundational type-theoretic account of typed structure editing, rather than an end-user tool itself. Hazelnut's rich metatheory, which we have mechanized in Agda, guides the definition of an extension to the calculus. The most plausible evaluation strategies for terms with holes reveal connections with gradual typing and contextual modal type theory (the Curry-Howard interpretation of contextual modal logic.) Furthermore, Hazelnut's semantics lends itself to implementation as a functional reactive program. A paper describing this topic will appear in the Symposium on the Principles of Programming Languages (POPL), 2017.
  .
• Usable formal methods for the design and composition of security and privacy policies. (Breaux, Niu (UTSA)). Three results: (1) Prototyping new survey design to collect information types from mobile app screens to expand ontological analysis of information flow tracing within apps and third-party servers. Completed pilot study of this new survey design (UTSA/CMU). (2) Extending semantic analysis techniques to infer ontological relationships in natural-language privacy policies. This includes extending dataset to larger number of policies, and investigating free-listing techniques and electroencephalogram (EEG) to measure human subject interpretations (CMU). (3) Generating policy specification statements by learning policy parameters from natural-language privacy policies and by analyzing API calls that handle private data in source code. The generated policy statement can then be formally composed into a policy specification (UTSA/CMU).
  
• Science of Secure Frameworks. (Garlan, Schmerl, Sunshine, Aldrich, Abi Antoun (Wayne State), Makek (UCI)). Two results: (1) We have been investigating more nuanced ways to describe and analyze self-protecting systems. These include: including different kinds of uncertainty into the models that we have of the system and the environment, doing a survey of different utility methods for deciding what to do and investigating the circumstances in which they apply, and understanding how to capture different kinds of security qualities (such as observability -- if a mitigation is observable to an attacker, or discoverability -- the degree to which an attacker can discover properties of a system after an adaptation). These ideas will be folded into our adaptation analytics capabilities. (2) We have been exploring the testing and identification of bugs that occur due to sequences of callbacks executed as part of a running Android app. We have built a preliminary analysis to identify such bugs related to resource locks (e.g., whether a lock that keeps a device awake is both acquired and released along program paths). To that end, we have been investigating a research prototype capable of determining static sequences of callbacks depending on the state of the Android platform. The approach has several applications in assessing the security properties of Android software, e.g., could potentially be used to execute malicious behaviors that occur only under certain conditions.
  Ab Antoun's Ph.D. student Khalaj passed his thesis proposal on July 28: http://www.cs.wayne.edu/~mabianto/inprep/16-khalaj.pdf
  .
• Race Vulnerability Study and Hybrid Race Detection (Aldrich, Srisa-an (Univ Nebraska Lincoln). : performed study on 20 participants using tool called Glacier. This study proved the success in the Java's final form of immutability as opposed to those who did not interacted with this tool. When multiple apps on an Android platform interact, faults and security vulnerabilities can occur. Software engineers need to be able to analyze interacting apps to detect such problems. Current approaches for performing such analyses, however, are unable to scale up to handle the numbers of apps that may need to considered, and thus, are impractical for application to real-world scenarios. We introduce JITANA, a program analysis framework designed to analyze multiple Android apps simultaneously. By using a class-loader based approach instead of a compiler-based approach such as SOOT, JITANA is able to simultaneously analyze large numbers of interacting apps, perform on-demand analysis of large libraries, and effectively analyze dynamically generated code. Empirical studies of JITANA show that it is substantially more efficient than a state-of-the-art approach, and that it can effectively and efficiently analyze complex apps including Facebook, PokemonGo, and Pandora. A paper describing this topic was submitted to the International Conference on Software Engineering (ICSE) 2017. Though immutability has been long-proposed as a way to prevent bugs in software, little is known about how to make immutability support in programming languages effective for software engineers. We designed a new formalism that extends Java to support transitive class immutability, the form of immutability for which there is the strongest empirical support, and implemented that formalism in a tool called Glacier. We applied Glacier successfully to two real-world systems. We also compared Glacier to Java's final in a user study of twenty participants. We found that even after being given instructions on how to express immutability with final, participants who used final were unable to express immutability correctly, whereas almost all participants who used Glacier succeeded. We also asked participants to make specific changes to immutable classes and found that participants who used final all incorrectly mutated immutable state, whereas almost all of the participants who used Glacier succeeded. Glacier represents a promising approach to enforcing immutability in Java and provides a model for enforcement in other languages. A paper describing this topic was submitted to the International Conference on Software Engineering (ICSE) 2017.
• Multi-Model Run-time Security Analysis. (Garlan, Schmerl, Pfeffer). Four results: (1) We have continued analysis of our path based anomaly detection algorithm to understand its strengths and limitations. This has involved (a) scaling up the size of the example to internet-scale systems. We can then generate large numbers of transactions to analyze; and (b) generating multiple examples of anomalies. These changes will allow us to investigate better the precision and recall of the anomaly detection, as well as the scale performance metrics. (2) We have continued specification of an example that will be useful for understanding run time defense deployment. This example is inspired by public knowledge about the Target point-of-scale security breach that leaked credit card information. The aim of the example is to provide a basis for reasoning about which security tactics could have been deployed at which stages of the attack, and to understand the trade-offs (in terms of cost, performance, observability) in deploying them. (3) We have developed software that generates large scale architectures from (in the order of a thousand software elements) from descriptions of architectures styles. We have applied this to a description of cloud-based amazon web service systems. This can be used as the basis of simulations for insider threat scenarios to test analysis of large scale systems. The system uses a combination of Acme architecture style rules encoded as an alloy model. Model checking is then used to generate example systems, which are then translated back into Acme for display and analysis. To get to scale, we developed a method of generating specific subsystems from Alloy specs and then stitching them together to come up with one large system. (4) Using these generated architectures, we aim to analyze the network structure that is created from the architecture design. We applied SNA techniques to compute traditional statistics such as betweenness centrality, closeness centrality, eigenvector centrality, clustering coefficient, and others. In future, we aim to compute advance statistics based on the network flow and usage patterns for both edges and nodes, to compute an overall statistic for the architecture to infer if the overall architecture has a 'bad smell' or not. To this end, we have written code for computing the basic SNA statistics.
  
• Highly configurable systems (Kastner). We interviewed six additional developers, reviewers, and policy makers regarding software security and safety certification practices using Common Criteria and DO178. Coded and classified issues, preparing discussion regarding security-related recertification and compositional certification. We studied attack vectors and mitigation through malicious package updates in software ecosystems of open source software, particularly Node.js/npm. We measured attack surface and evaluated feasibility of soundly verifying updates of small packages as free of certain attacks. With collaborators at Passau, we started a project to study the social dynamics of developer networks to better understand possible coordination problems or blindspots that cause failures to successfully address vulnerabilities in highly configurable systems. Using data from github and email networks used in the development process, we have so far investigated whether we can explain the growth of developer networks through preferential attachment, replicating a proposed network growth model but using a more rigorous maximum likelihood-based approach for statistical inference. We also have begun to explore specifications in Stochastic Actor-Oriented Models, a class of statistical network models that are on the cutting edge of being able to model the co-evolution of behavior and network structure. These will allow us to consider preferential attachment as a proposed explanation for network growth along with controls for reciprocity, transitivity, and node attributes.
  

Scientific Instrumentation - these highlights demonstrate new research to build the tools needed to conduct security experiments that could not previously have been performed.

• Tools to study long-term, security-related user behavior (Cranor, Christin, Acquisti, et al.). There are two major milestones to report: (1) In collaboration with Casey Canfield, a recent PhD graduate from CMU Engineering and Public Policy, we used field data from the Security Behavior Observatory (SBO) as well survey responses from SBO participants to assess the validity of signal detection theory in assessing participants' vulnerability to phishing attacks. We found there is evidence for the construct validity of signal detection theory for vulnerability to phishing attacks, but did not find evidence of predictive validity: signal detection measures of phishing vulnerability did not appear to be related to measures of security outcomes (e.g., counts of malware infection rates or visits to blacklisted URLs). (Results were submitted to CMH 2017.) (2) We completed development and began deployment to participants of the seventh version of our software. Resource usage monitoring to adjust sensor resource consumption (CPU, memory, disk, network) to avoid contention with user activities. This limits the impact of our sensors on the overall performance of our participants' computers. We also improved participant enrollment and management to reduce administrative costs of larger participant pool, and also we improved data transmission and storage to reduce server disk usage and improve server-side analysis performance.

B). Community Interaction

SAF|ART|INT. The Lablet sponsors agreed to provide modest funding to support the Carnegie Mellon Exploratory Workshop on Safety and Control for Artificial Intelligence, held on 27 June 2016. Results from this workshop informed the discussions at the workshop held the next day, 28 June 2016, that was co-sponsored by the White House Office of Science and Technology Policy (OSTP) and Carnegie Mellon.

Approximately 130 people from academia, industry, and government attended the Exploratory Workshop. Speakers included Ed Felten (OSTP), Bill Scherlis (CMU, chair), Eric Horvitz (Microsoft), Andrew Moore (CMU), Richar Mallah (Future of Life Inst), Tom Mitchell (CMU), Dario Amodei (Google), Claire Le Goues (CMU), and Robert Rahmer (IARPA). Speakers at the 28 June workshop included Ed Felten (White House OSTP), Bill Scherlis (CMU), Manuela Veloso (CMU), John Launchbury (DARPA), Jason Matheny (IARPA), Andy Grotto (White House NSC), Claire Tomlin (UC Berkeley), Tom Dietterich (Oregon State), Emma Brunskill (CMU), Michael Littman (Brown), Jeannette Wing (Microsoft), Kathleen Fisher (Tufts), Anupam Datta (CMU), Sarah Loos (Google), Mike Wagner (CMU), Drew Bagnell (Uber), Reid Simmons (NSF), Brian Murray (ZF), and Doug Schmidt (Vanderbilt).

Most talks from the workshop will be made avilable by video at the combined workshop website (www.cmu.edu/safartint/).

CMU ISR REU Program. CMU Lablet faculty leads (Josh Sunshine, Christian Kastner) are leading a summer program, Research Experience for Undergraduates (REU), sponsored by NSF. This is a highly competitive program -- more than one hundred students from diverse universities applied for 18 summer positions. These students are resident on campus and working with faculty in the Instiitute for Software Research, with many assigned to Lablet projects.

Kaestner keynote. Presented invited keynote at VACE workshop (Workshop on Variability and Complexity in Software Design) on quality assurance for highly configurable software systems (including security issues) in Austin, TX (May 2016).

C. Education

Prof Lorrie Cranor -- continues her work as Chief Technologist at the Federal Trade Commission. Cranor has arranged her schedule to be at CMU several days each week, allowing her to maintain continuity in her project. Nicolas Christin is acting Project Lead.

Transitions

Prof Robert Harper, who has been the project lead for epistemic models, has discontinued his work with the Lablet due to health issues. .