CMU SoS Lablet Quarterly Executive Summary - January 2019
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". These are the most important research accomplishments of the Lablet in the previous quarter.
Obsidian Project (Aldrich)
PUBLICATIONS
Michael Coblenz, Jonathan Aldrich, Brad A. Myers, Joshua Sunshine. Interdisciplinary Programming Language Design (Essay). InProc. of Onward!, 2018.
Paulette Koronkevich. Obsidian in the Rough: A Case Study Evaluation of a New Blockchain Programming Language. In SPLASH Student Research Competion, 2018. Awarded 2nd place.
PUBLIC ACCOMPLISHMENT HIGHLIGHTS
Blockchains have been proposed to support transactions with distributed and shared state. Despite design features meant to support security, security vulnerabilities in existing programs have been exploited by hackers. We are focusing on reducing implementation errors through the application of user-centered design in the creation of a new language, Obsidian, that uses typestate and linearity to support stronger safety guarantees than current approaches for programming blockchain systems.
Resilient architectures (Garlan)
PUBLIC ACCOMPLISHMENT HIGHLIGHTS
Planning for automated management of software systems often involves optimization with multiple objectives. In the optimization process, end-users and security administrators need to understand the expected consequences of candidate planning solutions, including the necessary tradeoffs made to reconcile competing objectives.
In the context of Markov decision process (MDP) planning, manually inspecting the solution policy and its value function to gain such understanding is infeasible due to the lack of domain semantics and concepts in which the end-users are interested. There is also a lack information about which of the objectives might be conflicting with each other in a problem instance, and what were the compromises that had to be made.
We investigated an approach to generate automated explanation of a MDP policy that is based on: (i) describing the expected consequences of the policy in terms of domain-specific, human-concept values, and relating those values to the overall expected cost of the policy, and (ii) explaining any tradeoff by contrasting the policy to counterfactual solutions (i.e., alternative policies that were not generated as a solution) on the basis of their human-concept values and the corresponding costs.
We demonstrate our approach on MDP problems with two different cost criteria, namely, the expected total-cost and average-cost criteria. Such an approach enhances resilient architectures by helping to explain and have stakeholders explore the decision making process that goes into automated planning for maintaining system resilience.
B. Community Engagement(s)
Research interaction in the community including workshops, seminars, competitions, etc.
Obsidian Project (Aldrich)
In many developing countries, farming insurance markets have not developed. A severe weather event such as an unexpected hard frost or a drought can therefore devastate farmers. We have started working with the World Bank to develop a parametric insurance platform on the Blockchain with Obsidian to address this need. The platform will serve as an evaluative case study of the expressiveness and effectiveness of the Obsidian language design.
C. Educational Advances
Impact to courses or curriculum at your school or elsewhere that indicates an increased training or rigor in security research.
N/A