publications

2023

1. TOSEM

   What’s (Not) Working in Programmer User Studies?

   Matthew C. Davis, Emad Aghayi, Thomas D. LaToza, Xiaoyin Wang, Brad A. Myers, and Joshua Sunshine

   ACM Transactions on Software Engineering and Methodology (TOSEM), 2023.

   Abstract PDF

   A key goal of software engineering research is to improve the environments, tools, languages, and techniques programmers use to efficiently create quality software. Successfully designing these tools and demonstrating their effectiveness involves engaging with tool users — software engineers. Researchers often want to conduct user studies of software engineers to collect direct evidence. However, running user studies can be difficult, and researchers may lack solution strategies to overcome the barriers, so they may avoid user studies. To understand the challenges researchers face when conducting programmer user studies, we interviewed 26 researchers. Based on the analysis of interview data we contribute: (i) a taxonomy of 18 barriers researchers encounter; (ii) 23 solution strategies some researchers use to address 8 of the 18 barriers in their own studies; and (iii) 4 design ideas, which we adapted from the behavioral science community, that may lower 8 additional barriers. To validate the design ideas, we held an in-person all-day focus group with 16 researchers.

2021

1. UIST

   ReCode: A Lightweight Find-and-Replace Interaction in the IDE for Transforming Code by Example

   Wode Ni, Joshua Sunshine, Vu Le, Sumit Gulwani, and Titus Barik

   In Proc. Symposium on User Interface Software and Technology (UIST), 2021.

   Abstract HTML PDF

   Software developers frequently confront a recurring challenge of making code transformations similar but not entirely identical code changes in many places in their integrated development environments. Through formative interviews (n = 7), we found that developers were aware of many tools intended to help with code transformations, but often made their changes manually because these tools required too much expertise or effort to be able to use effectively. To address these needs, we built an extension for Visual Studio Code, called reCode. reCode improves the familiar find-and-replace experience by allowing the developer to specify a straightforward search term to identify relevant locations, and then demonstrate their intended changes by simply typing a change directly in the editor. Using programming by example, reCode automatically learns a more general code transformation and displays these transformations as before-and-after differences inline, with clickable actions to interactively accept, reject, or refine the proposed changes. In our usability evaluation (n = 12), developers reported that this mixed-initiative, example-driven experience is intuitive, complements their existing workflow, and offers a unified approach to conveniently tackle a variety of common yet frustrating scenarios for code transformations.

2. CACM

   PL and HCI: Better Together

   Sarah E. Chasins, Elena L. Glassman, and Joshua Sunshine

   Commununications of the ACM (CACM), 2021.

   HTML PDF
3. ECOOP

   Gradual Program Analysis for Null Pointers

   Sam Estep, Jenna Wise, Jonathan Aldrich, Tanter, Johannes Bader, and Joshua Sunshine

   In Proc. Europoean Conference on Object-Oriented Programming (ECOOP), 2021.

   Abstract PDF

   Static analysis tools typically address the problem of excessive false positives by requiring programmers to explicitly annotate their code. However, when faced with incomplete annotations, many analysis tools are either too conservative, yielding false positives, or too optimistic, resulting in unsound analysis results. In order to flexibly and soundly deal with partially-annotated programs, we propose to build upon and adapt the gradual typing approach to abstract-interpretation-based program analyses. Specifically, we focus on null-pointer analysis and demonstrate that a gradual null-pointer analysis hits a sweet spot, by gracefully applying static analysis where possible and relying on dynamic checks where necessary for soundness. In addition to formalizing a gradual null-pointer analysis for a core imperative language, we build a prototype using the Infer static analysis framework, and present preliminary evidence that the gradual null-pointer analysis reduces false positives compared to two existing null-pointer checkers for Infer. Further, we discuss ways in which the gradualization approach used to derive the gradual analysis from its static counterpart can be extended to support more domains. This work thus provides a basis for future analysis tools that can smoothly navigate the tradeoff between human effort and run-time overhead to reduce the number of reported false positives.

4. TOCHI

   PLIERS: A Process That Integrates User-Centered Methods into Programming Language Design

   Michael Coblenz, Gauri Kambhatla, Paulette Koronkevich, Jenna L. Wise, Celeste Barnaby, Joshua Sunshine, Jonathan Aldrich, and Brad A. Myers

   ACM Transactions on Computer-Human Interaction (TOCHI), 2021.

   Abstract PDF

   Programming language design requires making many usability-related design decisions. However, existing HCI methods can be impractical to apply to programming languages: languages have high iteration costs, programmers require significant learning time, and user performance has high variance. To address these problems, we adapted both formative and summative HCI methods to make them more suitable for programming language design. We integrated these methods into a new process, PLIERS, for designing programming languages in a user-centered way. We assessed PLIERS by using it to design two new programming languages. Glacier extends Java to enable programmers to express immutability properties effectively and easily. Obsidian is a language for blockchains that includes verification of critical safety properties. Empirical studies showed that the PLIERS process resulted in languages that could be used effectively by many programmers and revealed additional opportunities for language improvement.

5. ICSE

   Containing Malicious Package Updates in npm with a Lightweight Permission System

   Gabriel Ferreira, Limin Jia, Joshua Sunshine, and Christian Kästner

   In Proc. International Conference on Software Engineering (ICSE), 2021.

   Abstract PDF

   The large amount of third-party packages available in fast-moving software ecosystems, such as Node.js/npm, enables attackers to compromise applications by pushing malicious updates to their package dependencies. Studying the npm repository, we observed that many packages in the npm repository that are used in Node.js applications perform only simple computations and do not need access to filesystem or network APIs. This offers the opportunity to enforce least-privilege design per package, protecting applications and package dependencies from malicious updates. We propose a lightweight permission system that protects Node.js applications by enforcing package permissions at runtime. We discuss the design space of solutions and show that our system makes a large number of packages much harder to be exploited, almost for free.

6. SANER

   FrameFix: Automatically Repairing Statically-Detected Directive Violations in Framework Applications

   Zack Coker, Joshua Sunshine, and Claire Le Goues

   2021.

   Abstract PDF

   Software frameworks make developing applications for a specific domain easier than doing so from scratch. Unfortunately, frameworks can also place unexpected requirements on a developer’s application, which can, in turn, lead to application bugs in the development process. We propose an automated technique for repairing violations of state-based framework requirements, FrameFix. First, developers of a framework can encode state-based framework requirements. Then, FrameFix automatically checks whether a developer’s application follows the encoded requirements. Once a violation of these requirements has been detected, FrameFix tries three different approaches - reordering method calls, moving method calls to different method definitions, and comparing the faulty method to similarly defined methods on GitHub. These repair approaches are based on the principles of how frameworks interact with framework applications: object protocols and inversion of control. To demonstrate that these principles can be used to aid automated repair for framework applications, we created a sample implementation of FrameFix for Android applications. Our evaluation shows that FrameFix is effective, repairing both real bugs in real applications, and a large number and variety of injected defects.

2020

1. OOPSLA

   Can advanced type systems be usable? An empirical study of ownership, assets, and typestate in obsidian

   Michael Coblenz, Jonathan Aldrich, Brad A Myers, and Joshua Sunshine

   Proceedings of the ACM on Programming Languages (OOPSLA), 2020. 🏆 Distinguished Artifact Award

   Abstract PDF

   Some blockchain programs (smart contracts) have included serious security vulnerabilities. Obsidian is a new typestate-oriented programming language that uses a strong type system to rule out some of these vulnerabilities. Although Obsidian was designed to promote usability to make it as easy as possible to write programs, strong type systems can cause a language to be difficult to use. In particular, ownership, typestate, and assets, which Obsidian uses to provide safety guarantees, have not seen broad adoption together in popular languages and result in significant usability challenges. We performed an empirical study with 20 participants comparing Obsidian to Solidity, which is the language most commonly used for writing smart contracts today. We observed that Obsidian participants were able to successfully complete more of the programming tasks than the Solidity participants. We also found that the Solidity participants commonly inserted asset-related bugs, which Obsidian detects at compile time.

2. OOPSLA

   Gradual Verification of Recursive Heap Data Structures

   Jenna Wise, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, and Joshua Sunshine

   Proceedings of the ACM on Programming Languages (OOPSLA), 2020.

   Abstract PDF

   Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, prior work proposed gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking. The prior approach to gradual verification, however, was limited to programs without recursive data structures. This paper extends gradual verification to programs that manipulate recursive, mutable data structures on the heap. We address several technical challenges, such as semantically connecting iso- and equi-recursive interpretations of abstract predicates, and supporting gradual verification of heap ownership. This work thus lays the foundation for future tools that work on realistic programs and support verification within an engineering process in which cost-benefit trade-offs can be made.

3. TOPLAS

   Obsidian: Typestate and Assets for Safer Blockchain Programming

   Michael Coblenz, Reed Oei, Tyler Etzel, Paulette Koronkevich, Miles Baker, Yannick Bloem, Brad A. Myers, Joshua Sunshine, and Jonathan Aldrich

   ACM Transactions on Programmming Languages and Systems (TOPLAS), 2020.

   Abstract PDF

   Blockchain platforms are coming into use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, supporting smart contracts, which maintain persistent state and support transactions that transform the state. Unfortunately, bugs in many smart contracts have been exploited by hackers. Obsidian is a novel programming language with a type system that enables static detection of bugs that are common in smart contracts today. Obsidian is based on a core calculus, Silica, for which we proved type soundness. Obsidian uses typestate to detect improper state manipulation and uses linear types to detect abuse of assets. We integrated a permissions system that encodes a notion of ownership to allow for safe, flexible aliasing. We describe two case studies that evaluate Obsidian’s applicability to the domains of parametric insurance and supply chain management, finding that Obsidian’s type system facilitates reasoning about high-level states and ownership of resources. We compared our Obsidian implementation to a Solidity implementation, observing that the Solidity implementation requires much boilerplate checking and tracking of state, whereas Obsidian does this work statically.

4. SIGGRAPH

   Penrose: From Mathematical Notation to Beautiful Diagrams

   Katherine Ye, Wode Ni, Max Krieger, Dor Ma’ayan, Jenna Wise, Jonathan Aldrich, Joshua Sunshine, and Keenan Crane

   ACM Transaction on Graphics (SIGGRAPH), 2020.

   Abstract PDF

   We introduce a system called Penrose for creating mathematical diagrams. Its basic functionality is to translate abstract statements written in familiar math-like notation into one or more possible visual representations. Rather than rely on a fixed library of visualization tools, the visual representation is user-defined in a constraint-based specification language; diagrams are then generated automatically via constrained numerical optimization. The system is user-extensible to many domains of mathematics, and is fast enough for iterative design exploration. In contrast to tools that specify diagrams via direct manipulation or low-level graphics programming, Penrose enables rapid creation and exploration of diagrams that faithfully preserve the underlying mathematical meaning. We demonstrate the effectiveness and generality of the system by showing how it can be used to illustrate a diverse set of concepts from mathematics and computer graphics.

5. CHI

   How Domain Experts Create Conceptual Diagrams and Implications for Tool Design

   Dor Ma’ayan, Wode Ni, Katherine Ye, Chinmay Kulkarni, and Joshua Sunshine

   In Proc. of the Conference on Human Factors in Computing Systems (CHI), 2020. 🏆 Best Paper Honourable Mention

   Abstract HTML PDF

   Conceptual diagrams are used extensively to understand abstract relationships, explain complex ideas, and solve difficult problems. To illustrate concepts effectively, experts find appropriate visual representations and translate concepts into concrete shapes. This translation step is not supported explicitly by current diagramming tools. This paper investigates how domain experts create conceptual diagrams via semi-structured interviews with 18 participants from diverse backgrounds. Our participants create, adapt, and reuse visual representations using both sketches and digital tools. However, they had trouble using current diagramming tools to transition from sketches and reuse components from earlier diagrams. Our participants also expressed frustration with the slow feedback cycles and barriers to automation of their tools. Based on these results, we suggest four opportunities of diagramming tools—exploration support, representation salience, live engagement, and vocabulary correspondence—that together enable a natural diagramming experience. Finally, we discuss possibilities to leverage recent research advances to develop natural diagramming tools.

6. PLATEAU

   Designing Declarative Language Tutorials: A Guided and Individualized Approach

   Anael Kuperwajs Cohen, Wode Ni, and Joshua Sunshine

   In Proc. Workshop at the Intersection Human-Computer Interaction and Programming Languages (PLATEAU), 2020.

   Abstract PDF

   The ability to declare what a program should include rather than how these features should be implemented makes declarative languages very useful in many visual output programs. The wide-ranging uses of these programs, in domains ranging from architecture to web programming to data visualization, encourages us to find an effective method to teach them. Traditional tutorial systems are usually non-interactive and have a gap between the learning and application. This can leave the user frustrated without a way to move forward in the learning process. A general lack of guidance can lead the student down an incorrect path. To prevent these difficulties, we propose a guided tour followed by novel question types that both direct the student’s learning and creates a focused environment to practice individual skills. Lastly, we propose a study to test the hypothesis that this tutorial is quicker to complete and results in a greater understanding of the declarative language.

7. PLATEAU

   A Pilot Study of the Safety and Usability of the Obsidian Blockchain Programming Language

   Gauri Kambhatla, Michael Coblenz, Reed Oei, Joshua Sunshine, Jonathan Aldrich, and Brad A. Myers

   In Proc. Workshop at the Intersection Human-Computer Interaction and Programming Languages (PLATEAU), 2020.

   Abstract PDF

   Although blockchains have been proposed for building systems that execute critical transactions, security vulnerabilities have plagued programs that are deployed on blockchain systems. The programming language Obsidian was developed with the purpose of statically preventing some of the more common of these security risks, specifically the loss of resources and improper manipulation of objects. The question then is whether Obsidian’s novel features impact the usability of the language. In this paper, we begin to evaluate Obsidian with respect to usability, and develop materials for a quantitative user study through a sequence of pilot studies. Specifically, our goal was to assess a) potential usability problems of Obsidian, b) the effectiveness of a tutorial for participants to learn the language, and c) the design of programming tasks to evaluate performance using the language. Our preliminary results tentatively suggest that the complexity of Obsidian’s features do not hinder usability, although these results will be validated in the quantitative study. We also observed the following factors as being important in a given programmer’s ability to learn Obsidian: a) integrating very frequent opportunities for practice of the material - e.g., after less than a page of material at a time, and b) previous programming experience and self-efficacy.

2019

1. WETSEB

   Smarter smart contract development tools

   Michael Coblenz, Joshua Sunshine, Jonathan Aldrich, and Brad Myers

   In Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), 2019.

   Abstract PDF

   Much recent work focuses on finding bugs and security vulnerabilities in smart contracts written in existing languages. Although this approach may be helpful, it does not address flaws in the underlying programming language, which can facilitate writing buggy code in the first place. We advocate a re-thinking of the blockchain software engineering tool set, starting with the programming language in which smart contracts are written. In this paper, we propose and justify requirements for a new generation of blockchain software development tools. New tools should (1) consider users’ needs as a primary concern; (2) seek to facilitate safe development by detecting relevant classes of serious bugs at compile time; (3) as much as possible, be blockchain-agnostic, given the wide variety of different blockchain platforms available, and leverage the properties that are common among blockchain environments to improve safety and developer effectiveness.

2. ICSE NIER

   Detecting suspicious package updates

   Kalil Garrett, Gabriel Ferreira, Limin Jia, Joshua Sunshine, and Christian Kästner

   In Proc. International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), 2019.

   Abstract PDF

   With an increased level of automation provided by package managers, which sometimes allow updates to be installed automatically, malicious package updates are becoming a real threat in software ecosystems. To address this issue, we propose an approach based on anomaly detection, to identify suspicious updates based on security-relevant features that attackers could use in an attack. We evaluate our approach in the context of Node.js/npm ecosystem, to show its feasibility in terms of reduced review effort and the correct identification of a confirmed malicious update attack. Although we do not expect it to be a complete solution in isolation, we believe it is an important security building block for software ecosystems.

3. VL/HCC

   Barriers to Reproducible Scientific Programming

   David Gray Widder, Joshua Sunshine, and Stephen Fickas

   In Proc. IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC), 2019.

   Abstract PDF

   Scientists often write code to support their science. To investigate the state of scientific programming on smaller teams in diverse scientific contexts, we interviewed eleven sci- entists about their programming practices, and the extent to which they adhere to six common best practices. We argue that these practices are essential to the core scientific value of reproducibility. Our results indicate that many of these practices are not followed because of barriers such as low self- efficacy and misaligned incentive structures. We conclude with suggested improvements to the tooling, education, and incentives of scientific programmers.

4. ICSME

   A qualitative study on framework debugging

   Zack Coker, David Gray Widder, Claire Le Goues, Christopher Bogart, and Joshua Sunshine

   In IEEE International Conference on Software Maintenance and Evolution (ICSME), 2019.

   Abstract PDF

   Features of frameworks, such as inversion of control and the structure of framework applications, require develop- ers to adjust their programming and debugging strategies as compared to sequential programs. However, the benefits and challenges of framework debugging are not fully understood, and gaining this knowledge could provide guidance in debugging strategies and framework tool design. To gain insight into the framework application debugging process, we performed two human studies investigating how developers fix applications that use a framework API incorrectly. These studies focused on the Android Fragment class and the ROS framework. We analyzed the results of the studies using a mixed-methods approach, using techniques from qualitative approaches. Our analysis found that participants benefited from the structure of frameworks and the pre-made solutions to common problems in the domain. Participants encountered challenges with understanding frame- work abstractions, and had particular difficulty with inversion of control and object protocol issues. When compared to prior work on debugging, these results show that framework applications have unique debugging challenges.

2018

1. Onward!

   Interdisciplinary programming language design

   Michael Coblenz, Jonathan Aldrich, Brad A Myers, and Joshua Sunshine

   In Proc. ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), 2018.

   Abstract PDF

   Approaches for programming language design used commonly in the research community today center around theoretical and performance-oriented evaluation. Recently, researchers have been considering more approaches to language design, including the use of quantitative and qualitative user studies that examine how different designs might affect programmers. In this paper, we argue for an interdisciplinary approach that incorporates many different methods in the creation and evaluation of programming languages. We argue that the addition of user-oriented design techniques can be helpful at many different stages in the programming language design process.

2. FM

   IPL: An integration property language for multi-model cyber-physical systems

   Ivan Ruchkin, Joshua Sunshine, Grant Iraci, Bradley Schmerl, and David Garlan

   In Proc. International Symposium on Formal Methods (FM), 2018.

   Abstract PDF

   Design and verification of modern systems requires diverse models, which often come from a variety of disciplines, and it is challenging to manage their heterogeneity – especially in the case of cyber-physical systems. To check consistency between models, recent approaches map these models to flexible static abstractions, such as architectural views. This model integration approach, however, comes at a cost of reduced expressiveness because complex behaviors of the models are abstracted away. As a result, it may be impossible to automatically verify important behavioral properties across multiple models, leaving systems vulnerable to subtle bugs. This paper introduces the Integration Property Language (IPL) that improves integration expressiveness using modular verification of properties that depend on detailed behavioral semantics while retaining the ability for static system-wide reasoning. We prove that the verification algorithm is sound and analyze its termination conditions. Furthermore, we perform a case study on a mobile robot to demonstrate IPL is practically useful and evaluate its performance.

3. SAC

   Experience report: Studying the readability of a domain specific language

   Johann Thor Mogensen Ingibergsson, Stefan Hanenberg, Joshua Sunshine, and Ulrik Pagh Schultz

   In Proc. ACM Symposium on Applied Computing (SAC), 2018.

   Abstract PDF

   Domain-specific languages (DSLs) are commonly expected to improve communication with domain experts compared to general-purpose programming languages (GPLs). However, there is a huge gap in the literature concerning how evidence can be given for this expected improvement—a phenomenon that is not only known from DSLs, but also from GPLs in general. This paper presents an experience report of applying an iterative process for evaluating DSL readability for a given DSL in the context of safety-critical software in robotics. The goal of this process is to conduct a randomized controlled trial that gives evidence for the better readability of the DSL in comparison to the readability of a GPL. In this experience report, we describe common pitfalls we identified and possible solutions to overcome these problems in the future.

4. HCI Blockchain

   User-centered design of permissions, typestate, and ownership in the Obsidian blockchain language

   Michael Coblenz, Jonathan Aldrich, Joshua Sunshine, and Brad A Myers

   In Workshop on HCI for Blockchain: Studying, Designing, Critiquing and Envisioning Distributed Ledger Technologies, 2018.

   Abstract PDF

   Blockchains have been proposed to support transactions on distributed, shared state, but hackers have exploited security vulnerabilities in existing programs. In this paper, we describe how we are applying user-centered design in the creation of Obsidian, a new language that uses typestate and linearity to support stronger safety guarantees than current approaches for programming blockchain systems. We show how an iterative, user-centered design process can be used to elicit design feedback and show how we incorporated that feedback into the language. We found that formative user studies, even with a small number of participants, can lead to useful insights in language design. The study results motivated important language changes, such as adding explicit ownership transfer syntax and changing the structure of state initialization in state transitions.

5. HCI Blockchain

   User-centered design of permissions, typestate, and ownership in the Obsidian blockchain language

   Michael Coblenz, Jonathan Aldrich, Joshua Sunshine, and Brad A Myers

   In Workshop on HCI for Blockchain: Studying, Designing, Critiquing and Envisioning Distributed Ledger Technologies, 2018.

   Abstract PDF

   Blockchains have been proposed to support transactions on distributed, shared state, but hackers have exploited security vulnerabilities in existing programs. In this paper, we describe how we are applying user-centered design in the creation of Obsidian, a new language that uses typestate and linearity to support stronger safety guarantees than current approaches for programming blockchain systems. We show how an iterative, user-centered design process can be used to elicit design feedback and show how we incorporated that feedback into the language. We found that formative user studies, even with a small number of participants, can lead to useful insights in language design. The study results motivated important language changes, such as adding explicit ownership transfer syntax and changing the structure of state initialization in state transitions.

2017

1. ICSE

   Glacier: Transitive class immutability for Java

   Michael Coblenz, Whitney Nelson, Jonathan Aldrich, Brad Myers, and Joshua Sunshine

   In Proc. International Conference on Software Engineering (ICSE), 2017.

   Abstract PDF

   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.

2. OBT

   Designing extensible, domain-specific languages for mathematical diagrams

   Katherine Ye, Keenan Crane, Jonathan Aldrich, and Joshua Sunshine

   POPL Off the Beaten Track Workshop, 2017.

   PDF
3. DSLDI

   SUBSTANCE and STYLE: domain-specific languages for mathematical diagrams

   Wode Ni, Katherine Ye, Joshua Sunshine, Jonathan Aldrich, and Keenan Crane

   Domain-Specific Language Design and Implementation (DSLDI), 2017.

   Abstract PDF

   Creating mathematical diagrams is essential for both developing one’s intuition and conveying it to others. However, formalizing diagrams in most general-purpose tools requires painstaking low-level manipulation of shapes and positions. We report on early work on PENROSE, a system we are building to automatically visualize mathematics from notation. PENROSE comprises two languages: SUBSTANCE, a domain-specific language that mimics the declarativeness of mathematical notation, and STYLE, a styling language that concisely specifies the visual semantics of the notation. Our system can automatically visualize set theory expressions with user-defined styles, and it can visualize abstract definitions of functions by producing concrete examples. We plan to extend the system to more domains of math.

4. SecDev

   Empirical studies on the security and usability impact of immutability

   Sam Weber, Michael Coblenz, Brad Myers, Jonathan Aldrich, and Joshua Sunshine

   In Proc. IEEE Cybersecurity Development (SecDev), 2017.

   Abstract PDF

   Although it is well-known that API design has a large and long-term impact on security, the literature contains few substantial guidelines for practitioners on how to design APIs that improve security. Even fewer of those guidelines have been evaluated empirically. Security professionals have proposed that software engineers choose immutable APIs and architectures to enhance security. Unfortunately, prior empirical research argued that immutablity decreases API usability. This paper brings together the results from a number of previous papers that together aim to show that immutability, when carefully designed using usability as a first-class requirement, can have positive effects on both usability and security. We also make observations on study design in this field.

5. PLATEAU

   A user study to inform the design of the obsidian blockchain dsl

   Celeste Barnaby, Michael Coblenz, Tyler Etzel, Eliezer Kanal, Joshua Sunshine, Brad Myers, and Jonathan Aldrich

   In Proc. Workshop at the Intersection Human-Computer Interaction and Programming Languages (PLATEAU), 2017.

   Abstract PDF

   Blockchain platforms such as Ethereum and Hyperledger facilitate transactions between parties that have not established trust. Increased interest in these platforms has motivated the design of programming languages such as Solidity, which allow users to create blockchain programs. However, there have been several recent instances where Solidity programs have contained bugs that have been exploited. The security of blockchain programs is especially important given that they commonly involve the exchange of money or other objects with real-world value. We are currently developing a blockchain-based programming language called Obsidian with the goal of minimizing the risk of common security vulnerabilities. We are designing this language in a humancentered way, conducting exploratory user studies with a natural programming approach to inform our design choices. In this paper, we discuss our approach to the design of a user study, as well as our preliminary findings.

2016

1. PeerJ CS

   A systematic analysis of the science of sandboxing

   Michael Maass, Adam Sales, Benjamin Chung, and Joshua Sunshine

   PeerJ Computer Science, 2016.

   Abstract HTML PDF

   Sandboxes are increasingly important building materials for secure software systems. In recognition of their potential to improve the security posture of many systems at various points in the development lifecycle, researchers have spent the last several decades developing, improving, and evaluating sandboxing techniques. What has been done in this space? Where are the barriers to advancement? What are the gaps in these efforts? We systematically analyze a decade of sandbox research from five top-tier security and systems conferences using qualitative content analysis, statistical clustering, and graph-based metrics to answer these questions and more. We find that the term “sandbox” currently has no widely accepted or acceptable definition. We use our broad scope to propose the first concise and comprehensive definition for “sandbox” that consistently encompasses research sandboxes. We learn that the sandboxing landscape covers a range of deployment options and policy enforcement techniques collectively capable of defending diverse sets of components while mitigating a wide range of vulnerabilities. Researchers consistently make security, performance, and applicability claims about their sandboxes and tend to narrowly define the claims to ensure they can be evaluated. Those claims are validated using multi-faceted strategies spanning proof, analytical analysis, benchmark suites, case studies, and argumentation. However, we find two cases for improvement: (1) the arguments researchers present are often ad hoc and (2) sandbox usability is mostly uncharted territory. We propose ways to structure arguments to ensure they fully support their corresponding claims and suggest lightweight means of evaluating sandbox usability.

2. ICSE

   Exploring language support for immutability

   Michael Coblenz, Joshua Sunshine, Jonathan Aldrich, Brad Myers, Sam Weber, and Forrest Shull

   In Proc. International Conference on Software Engineering (ICSE), 2016.

   Abstract PDF

   Programming languages can restrict state change by preventing it entirely (immutability) or by restricting which clients may modify state (read-only restrictions). The benefits of immutability and read-only restrictions in software structures have been long-argued by practicing software engineers, researchers, and programming language designers. However, there are many proposals for language mechanisms for restricting state change, with a remarkable diversity of techniques and goals, and there is little empirical data regarding what practicing software engineers want in their tools and what would benefit them. We systematized the large collection of techniques used by programming languages to help programmers prevent undesired changes in state. We interviewed expert software engineers to discover their expectations and requirements, and found that important requirements, such as expressing immutability constraints, were not reflected in features available in the languages participants used. The interview results informed our design of a new language extension for specifying immutability in Java. Through an iterative, participatory design process, we created a tool that reflects requirements from both our interviews and the research literature.

3. MSR

   Inter-app communication in android: Developer challenges

   Waqar Ahmad, Christian Kästner, Joshua Sunshine, and Jonathan Aldrich

   In Proc. Working Conference on Mining Software Repositories (MSR), 2016.

   Abstract PDF

   The Android platform is designed to support mutually un-trusted third-party apps, which run as isolated processes but may interact via platform-controlled mechanisms, called Intents. Interactions among third-party apps are intended and can contribute to a rich user experience, for example, the ability to share pictures from one app with another. The Android platform presents an interesting point in a design space of module systems that is biased toward isolation, extensibility, and untrusted contributions. The Intent mechanism essentially provides message channels among modules, in which the set of message types is extensible. However, the module system has design limitations including the lack of consistent mechanisms to document message types, very limited checking that a message conforms to its specifications, the inability to explicitly declare dependencies on other modules, and the lack of checks for backward compatibility as message types evolve over time. In order to understand the degree to which these design limitations result in real issues, we studied a broad corpus of apps and cross-validated our results against app documentation and Android support forums. Our findings suggest that design limitations do in- deed cause development problems. Based on our results, we outline further research questions and propose possible mitigation strategies.

4. ESEM

   Software development practices, barriers in the field and the relationship to software quality

   Beth Yost, Michael Coblenz, Brad Myers, Joshua Sunshine, Jonathan Aldrich, Sam Weber, Matthew Patron, Melissa Heeren, Shelley Krueger, and Mark Pfaff

   In Proc. ACM/IEEE Symposium on Empirical Software Engineering and Measurement (ESEM), 2016.

   Abstract PDF

   Context: Critical software systems developed for the government continue to be of lower quality than expected, despite extensive literature describing best practices in software engineering. Goal: We wanted to better understand the extent of certain issues in the field and the relationship to software quality. Method: We surveyed fifty software development professionals and asked about practices and barriers in the field and the resulting software quality. Results: There is evidence of certain problematic issues for developers and specific quality characteristics that seem to be affected. Conclusions: This motivates future work to address the most problematic barriers and issues impacting software quality.

2015

1. ICPC

   Searching the state space: A qualitative study of API protocol usability

   Joshua Sushine, James D Herbsleb, and Jonathan Aldrich

   In IEEE International Conference on Program Comprehension (ICPC), 2015.

   Abstract PDF

   Application Programming Interfaces (APIs) often define protocols – restrictions on the order of client calls to API methods. API protocols are common and difficult to use, which has generated tremendous research effort in alternative specification, implementation, and verification techniques. However, little is understood about the barriers programmers face when using these APIs, and therefore the research effort may be misdirected. To understand these barriers better, we perform a two-part qualitative study. First, we study developer forums to identify problems that developers have with protocols. Second, we perform a think-aloud observational study, in which we systematically observe professional programmers struggle with these same problems to get more detail on the nature of their struggles and how they use available resources. In our observations, programmer time was spent primarily on four types of searches of the protocol state space. These observations suggest protocol-targeted tools, languages, and verification techniques will be most effective if they enable programmers to efficiently perform state search.

2. VL/HCC

   A course-based usability analysis of Cilk Plus and OpenMP

   Michael Coblenz, Robert Seacord, Brad Myers, Joshua Sunshine, and Jonathan Aldrich

   In Proc. IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC), 2015.

   Abstract PDF

   Cilk Plus and OpenMP are parallel language extensions for the C and C++ programming languages. The CPLEX Study Group of the ISO/IEC C Standards Committee is developing a proposal for a parallel programming extension to C that combines ideas from Cilk Plus and OpenMP. We conducted a preliminary comparison of Cilk Plus and OpenMP in a master’s level course on security to evaluate the design tradeoffs in the usability and security of these two approaches. The eventual goal is to inform decision-making within the committee. We found several usability problems worthy of further investigation based on student performance, including declaring and using reductions, multi-line compiler directives, and the understanda-bility of task assignment to threads.

3. ACSAC

   Evaluating the flexibility of the Java sandbox

   Zack Coker, Michael Maass, Tianyuan Ding, Claire Le Goues, and Joshua Sunshine

   In Proc. Annual Computer Security Applications Conference (ACSAC), 2015.

   Abstract PDF

   The ubiquitously-installed Java Runtime Environment (JRE) provides a complex, flexible set of mechanisms that support the execution of untrusted code inside a secure sandbox. However, many recent exploits have successfully escaped the sandbox, allowing attackers to infect numerous Java hosts. We hypothesize that the Java security model affords developers more flexibility than they need or use in practice, and thus its complexity compromises security without improving practical functionality. We describe an empirical study of the ways benign open-source Java applications use and interact with the Java security manager. We found that developers regularly misunderstand or misuse Java security mechanisms, that benign programs do not use all of the vast flexibility afforded by the Java security model, and that there are clear differences between the ways benign and exploit programs interact with the security manager. We validate these results by deriving two restrictions on application behavior that restrict (1) security manager modifications and (2) privilege escalation. We demonstrate that enforcing these rules at runtime stop a representative proportion of modern Java 7 exploits without breaking backwards compatibility with benign applications. These practical rules should be enforced in the JRE to fortify the Java sandbox.

4. PLATEAU

   Comparing transitive to non-transitive object immutability

   Michael Coblenz, Joshua Sunshine, Brad A Myers, Sam Weber, and Forrest Shull

   In Proc. Workshop at the Intersection Human-Computer Interaction and Programming Languages (PLATEAU), 2015.

   Abstract PDF

   Many programming languages provide features that express restrictions on which data structures can be changed. For example, C++ includes const and Java includes final. Languages that are in widespread use typically provide non-transitive immutability: when a reference is specified to be immutable or read-only, the object referenced can still reference mutable structures. However, some languages, particularly research languages, provide transitive immutability, in which immutable objects can only reference other immutable objects (with some exceptions). We are designing a lab study of programmers to elucidate the differences in programmer effectiveness between these two approaches.

5. MobileDeLi

   Enforcing fine-grained security and privacy policies in an ecosystem within an ecosystem

   Waqar Ahmad, Joshua Sunshine, Christian Kästner, and Adam Wynne

   In Workshop on Mobile Development Lifecycle (MobileDeLi), 2015.

   Abstract PDF

   Smart home automation and IoT promise to bring many advantages but they also expose their users to certain security and privacy vulnerabilities. For example, leaking the information about the absence of a person from home or the medicine somebody is taking may have serious security and privacy consequences for home users and potential legal implications for providers of home automation and IoT platforms. We envision that a new ecosystem within an existing smartphone ecosystem will be a suitable platform for distribution of apps for smart home and IoT devices. Android is increasingly becoming a popular platform for smart home and IoT devices and applications. Built-in security mechanisms in ecosystems such as Android have limitations that can be exploited by malicious apps to leak users’ sensitive data to unintended recipients. For instance, Android enforces that an app requires the Internet permission in order to access a web server but it does not control which servers the app talks to or what data it shares with other apps. Therefore, sub-ecosystems that enforce additional fine-grained custom policies on top of existing policies of the smartphone ecosystems are necessary for smart home or IoT platforms. To this end, we have built a tool that enforces additional policies on inter-app interactions and permissions of Android apps. We have done preliminary testing of our tool on three proprietary apps developed by a future provider of a home automation platform. Our initial evaluation demonstrates that it is possible to develop mechanisms that allow definition and enforcement of custom security policies appropriate for ecosystems of the like smart home automation and IoT.

2014

1. TOPLAS

   Æminium: A permission-based concurrent-by-default programming language approach

   Sven Stork, Karl Naden, Joshua Sunshine, Manuel Mohr, Alcides Fonseca, Paulo Marques, and Jonathan Aldrich

   ACM Transactions on Programmming Languages and Systems (TOPLAS), 2014.

   Abstract PDF

   Writing concurrent applications is extremely challenging, not only in terms of producing bug-free and maintainable software, but also for enabling developer productivity. In this article we present the Æminium concurrent-by-default programming language. Using Æminium programmers express data dependencies rather than control flow between instructions. Dependencies are expressed using permissions, which are used by the type system to automatically parallelize the application. The Æminium approach provides a modular and composable mechanism for writing concurrent applications, preventing data races in a provable way. This allows programmers to shift their attention from low-level, error-prone reasoning about thread interleaving and synchronization to focus on the core functionality of their applications. We study the semantics of Æminium through μÆminium, a sound core calculus that leverages permission flow to enable concurrent-by-default execution. After discussing our prototype implementation we present several case studies of our system. Our case studies show up to 6.5X speedup on an eight-core machine when leveraging data group permissions to manage access to shared state, and more than 70% higher throughput in a Web server application.

2. ECOOP

   Structuring documentation to support state search: A laboratory experiment about protocol programming

   Joshua Sunshine, James D Herbsleb, and Jonathan Aldrich

   In Proc. Europoean Conference on Object-Oriented Programming (ECOOP), 2014.

   Abstract PDF

   Application Programming Interfaces (APIs) often define object protocols. Objects with protocols have a finite number of states and in each state a different set of method calls is valid. Many researchers have developed protocol verification tools because protocols are notoriously difficult to follow correctly. However, recent research suggests that a major challenge for API protocol programmers is effectively searching the state space. Verification is an ineffective guide for this kind of search. In this paper we instead propose Plaiddoc, which is like Javadoc except it organizes methods by state instead of by class and it includes explicit state transitions, state-based type specifications, and rich state relationships. We compare Plaiddoc to a Javadoc control in a between-subjects laboratory experiment. We find that Plaiddoc participants complete state search tasks in significantly less time and with significantly fewer errors than Javadoc participants.

3. PLATEAU

   Considering Productivity Effects of Explicit Type Declarations

   Michael Coblenz, Jonathan Aldrich, Brad Myers, and Joshua Sunshine

   In Proc. Workshop at the Intersection Human-Computer Interaction and Programming Languages (PLATEAU), 2014.

   Abstract PDF

   Static types may be used both by the language implementation and directly by the user as documentation. Though much existing work focuses primarily on the implications of static types on the semantics of programs, relatively little work considers the impact on usability that static types provide. Though the omission of static type information may decrease program length and thereby improve readability, it may also decrease readability because users must then frequently derive type information manually while reading programs. As type inference becomes more popular in languages that are in widespread use, it is important to consider whether the adoption of type inference may impact productivity of developers.

4. PLATEAU

   Usability Hypotheses in the Design of Plaid

   Joshua Sunshine, and Jonathan Aldrich

   In Proc. Workshop at the Intersection Human-Computer Interaction and Programming Languages (PLATEAU), 2014.

   Abstract PDF

   Plaid is a research programming language with a focus on typestate, permissions, and concurrency. Typestate describes ordering constraints on method calls to an object; Plaid incorporates typestate into both its object model and its type system. Permissions, incorporated into Plaid’s type system and runtime, describe whether a reference can be aliased and whether aliases can change that reference. Permissions support static typestate checking, but they also allow Plaid’s compiler to automatically parallelize Plaid code. In this paper, we describe the usability-related hypotheses that drove the design of Plaid. We describe the evidence, both informal and scientific, that inspired and (in some cases) validated these hypotheses, and reflect on our experience designing and validating the language.

2013

1. PhD Thesis

   Protocol Programmability

   Joshua Sunshine

   2013.

   Abstract PDF

   Application Programming Interfaces (APIs) often define protocols—restrictions on the order of client calls to API methods. API protocols are common and difficult to follow, which has generated tremendous research into the specification and verification of protocols. However, verification techniques do little to alleviate several major challenges programmers face when using API protocols: fixing protocol violations, learning protocol rules, and finding state transitions. To understand these challenges better, I mined developer forums to identify problems that developers have with protocols. Then, I performed a think-aloud observational study, in which I systematically observed professional programmers struggle with these same problems to get more detail on the nature of their struggles and how they used available resources. In my observations, programmer time was spent primarily on four types of searches of the protocol state space. To alleviate the protocol programmability challenges, I embed state modeling techniques directly into code and developer documentation. I design and formalize a programming language, Plaid, in which objects are modeled not just in terms of classes, but in terms of changing abstract states. Each state may have its own fields and methods, as well as methods that transition the object into a new state. I also developed a documentation tool called Plaiddoc, which is like Javadoc except it organizes methods by state instead of by class and it includes explicit state transitions, state-based type specifications, and rich state relationships. I evaluate Plaid through a series of examples taken from the Plaid compiler and standard libraries of Smalltalk and Java. These examples show how Plaid can more closely model state-based designs, enhancing understandability, automating error checking, and providing reuse benefits. I evaluate Plaiddoc with a user experiment and show that participants using Plaiddoc can perform state search significantly more quickly and accurately than participants using Javadoc.

2012

1. Technical Report

   The Plaid language: Typed core specification

   Jonathan Aldrich, Nels E Beckman, Robert Bocchino, Karl Naden, Darpan Saini, Sven Stork, and Joshua Sunshine

   2012.

   Abstract PDF

   Plaid is an object oriented programming language built on two paradigms. First, Plaid is typestate-oriented. Programmers can directly encode the abstract states of objects and use the state change operator to change the state, interface, and representation of an object at runtime. Second, Plaids type system is permission-based. The type of each reference includes an access permission which dictates how the reference can be used and characterizes the permissions to other aliases of the same object. Plaid leverages permissions when tracking the abstract state of references during typechecking. Permissions are also used to infer code that can be safely run in parallel. This document defines the core of the Plaid language, including its source syntax, the semantics of operations involving abstract states, and a type system.

2011

1. OOPSLA

   First-class state change in plaid

   Joshua Sunshine, Karl Naden, Sven Stork, Jonathan Aldrich, and Éric Tanter

   In Proc. ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications (OOSPLA), 2011.

   Abstract PDF

   Objects model the world, and state is fundamental to a faithful modeling. Engineers use state machines to understand and reason about state transitions, but programming languages provide little support for building software based on state abstractions. We propose Plaid, a language in which objects are modeled not just in terms of classes, but in terms of changing abstract states. Each state may have its own representation, as well as methods that may transition the object into a new state. A formal model precisely defines the semantics of core Plaid constructs such as state transition and trait-like state composition. We evaluate Plaid through a series of examples taken from the Plaid compiler and the standard libraries of Smalltalk and Java. These examples show how Plaid can more closely model state-based designs, enhancing understandability, enhancing dynamic error checking, and providing reuse benefits.

2. ICSE NIER

   Permission-based programming languages

   Jonathan Aldrich, Ronald Garcia, Mark Hahnenberg, Manuel Mohr, Karl Naden, Darpan Saini, Sven Stork, Joshua Sunshine, Éric Tanter, and Roger Wolff

   In Proc. International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), 2011.

   Abstract PDF

   Linear permissions have been proposed as a lightweight way to specify how an object may be aliased, and whether those aliases allow mutation. Prior work has demonstrated the value of permissions for addressing many software engineering concerns, including information hiding, protocol checking, concurrency, security, and memory management. We propose the concept of a permission-based programming language - a language whose object model, type system, and runtime are all co-designed with permissions in mind. This approach supports an object model in which the structure of an object can change over time, a type system that tracks changing structure in addition to addressing the other concerns above, and a runtime system that can dynamically check permission assertions and leverage permissions to parallelize code. We sketch the design of the permission-based programming language Plaid, and argue that the approach may provide significant software engineering benefits.

2010

1. FTfJP

   A theory of typestate-oriented programming

   Darpan Saini, Joshua Sunshine, and Jonathan Aldrich

   In Proc. Workshop on Formal Techniques for Java-Like Programs (FTfJP), 2010.

   Abstract PDF

   Engineers in many disciplines use state machines to reason about system changes, and many object-oriented libraries require their clients to follow state machine protocols. No existing language, however, has native support for state machines, and programmers often lose productivity and introduce errors when trying to understand and follow interaction protocols. The Plaid language extends the object paradigm with explicit states and state transitions, in order to better model object state transitions. In this paper, we present Plaidcore, a core calculus for Plaid, which uses states and permissions to statically guarantee that clients use object protocols correctly.

2. APLWACA

   DynXML: Safely programming the dynamic web

   Joshua Sunshine, and Jonathan Aldrich

   In Proc. Workshop on Analysis and Programming Languages for Web Applications and Cloud Applications (APLWACA), 2010.

   Abstract PDF

   A single web page in a complex web application has a huge number of possible runtime states. Functions, like JavaScript event handlers, that operate on such pages are extremely difficult to write correctly, because there are virtually no guaranteed constraints on the page. In this paper we propose DynXML, a new language for the web which safely and naturally mutates XML trees. Any dynamic web application written in DynXML is statically guaranteed to maintain the page in a subtype of a programmer-defined page type. Furthermore, event handlers are guaranteed to receive the page in the state they expect and leave it in the form expected by the next set of handlers—DynXML prevents page-manipulating programs from going wrong.

2009

1. USENIX security

   Crying Wolf: An Empirical Study of SSL Warning Effectiveness.

   Joshua Sunshine, Serge Egelman, Hazim Almuhimedi, Neha Atri, and Lorrie Faith Cranor

   In Proc. USENIX security symposium, 2009.

   Abstract PDF

   Web users are shown an invalid certificate warning when their browser cannot validate the identity of the websites they are visiting. While these warnings often appear in benign situations, they can also signal a man-in-the-middle attack. We conducted a survey of over 400 Internet users to examine their reactions to and understanding of current SSL warnings. We then designed two new warnings using warnings science principles and lessons learned from the survey. We evaluated warnings used in three popular web browsers and our two warnings in a 100- participant, between-subjects laboratory study. Our warnings performed significantly better than existing warnings, but far too many participants exhibited dangerous behavior in all warning conditions. Our results suggest that, while warnings can be improved, a better approach may be to minimize the use of SSL warnings altogether by blocking users from making unsafe connections and eliminating warnings in benign situations.

2. Onward!

   Typestate-oriented programming

   Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks

   In Proc. ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), 2009.

   Abstract PDF

   Objects model the world, and state is fundamental to a faithful modeling. Engineers use state machines to understand and reason about state transitions, but programming languages provide little support for reasoning about or implementing these state machines, causing software defects and lost productivity when objects are misused. We propose Typestate-Oriented Programming as a natural extension to the object paradigm, where objects are modeled not just in terms of classes, but in terms of changing states. Each state may have its own representation and methods which may transition the object into a new state. A flow-sensitive, permission-based type system helps developers track which state objects are in. First-class typestates are a powerful abstraction that will help developers model and reuse objects more efficiently and correctly.

3. DO21

   Language support for distributed proxies

   Darpan Saini, Joshua Sunshine, and Jonathan Aldrich

   In Proc. Workshop on Distributed Objects for the 21st Century (DO21), 2009.

   Abstract PDF

   Proxies are ubiquitous in distributed systems. They are mainly used to provide transparent access to server objects, and in some cases for additional functions such as caching, message routing, marshalling, and un-marshalling of data. In this paper, we discuss several software engineering problems associated with using proxies in a distributed system. We believe that proxies in distributed systems suffer from: 1) redundant code 2) multiple data translations that have to be written before data is marshalled for transfer over the wire, and 3) in the case when proxies are automatically generated, there is no universal or generic mapping (to date) from XML types to Object types and vice versa. We describe these problems using an example, and discuss the partial solutions provided by prior research. A better understanding of these problems may help show the way towards a future solution.

2002

1. EMBO Journal

   Molecular architecture and mechanism of an icosahedral pyruvate dehydrogenase complex: a multifunctional catalytic machine

   Jacqueline LS Milne, Dan Shi, Peter B Rosenthal, Joshua S Sunshine, Gonzalo J Domingo, Xiongwu Wu, Bernard R Brooks, Richard N Perham, Richard Henderson, and Sriram Subramaniam

   The EMBO journal, 2002.

   Abstract HTML PDF

   Electron cryo‐microscopy of ‘single particles’ is a powerful method to determine the three‐dimensional (3D) architectures of complex cellular assemblies. The pyruvate dehydrogenase multi‐enzyme complex couples the activity of three component enzymes (E1, E2 and E3) in the oxidative decarboxylation of pyruvate to generate acetyl‐CoA, linking glycolysis and the tricarboxylic acid cycle. We report here a 3D model for an 11 MDa, icosahedral pyruvate dehydrogenase sub‐complex, obtained by combining a 28 Å structure derived from electron cryo‐microscopy with previously determined atomic coordinates of the individual E1 and E2 components. A key feature is that the E1 molecules are located on the periphery of the assembly in an orientation that allows each of the 60 mobile lipoyl domains tethered to the inner E2 core to access multiple E1 and E2 active sites from inside the icosahedral complex. This unexpected architecture provides a highly efficient mechanism for active site coupling and catalytic rate enhancement by the motion of the lipoyl domains in the restricted annular region between the inner core and outer shell of the complex.