Web applications are governed by privacy policies, but developers lack practical abstractions to ensure that their code actually abides by these policies. This leads to frequent oversights, bugs, and costly privacy violations.

Increasing demand on computer networks continuously pushes manufacturers to incorporate novel features and capabilities into their switches at an ever-accelerating pace. However, the traditional approach to switch development relies on informal specifications and handcrafted tests to ensure reliability, which are tedious and slow to maintain and update, effectively putting feature velocity at odds with reliability.

An essential component of initiatives that aim to address pervasive inequalities of any kind is the ability to collect empirical evidence of both the status quo baseline and of any improvement that can be attributed to prescribed and deployed interventions. Unfortunately, two substantial barriers can arise preventing the collection and analysis of such empirical evidence: (1) the sensitive nature of the data itself and (2) a lack of technical sophistication and infrastructure available to both an initiative's beneficiaries and to those spearheading it. In the last few years, it has been shown that a cryptographic primitive called secure multi-party computation (MPC) can provide a natural technological resolution to this conundrum. MPC allows an otherwise disinterested third party to contribute its technical expertise and resources, to avoid incurring any additional liabilities itself, and (counterintuitively) to reduce the level of data exposure that existing parties must accept to achieve their data analysis goals. However, achieving these benefits requires the deliberate design of MPC tools and frameworks whose level of accessibility to non-technical users with limited infrastructure and expertise is state-of-the-art. We describe our own experiences designing, implementing, and deploying such usable web applications for secure data analysis within the context of two real-world initiatives that focus on promoting economic equality.

We consider the subtractive model repair problem : given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M ′ that satisfies η. Thus, M can be “repaired” to satisfy eta by deleting some transitions and states. We map an instance 〈 M ,η 〉 of model repair to a Boolean formula repair ( M ,η) such that 〈 M ,η 〉 has a solution iff repair ( M ,η) is satisfiable. Furthermore, a satisfying assignment determines which states and transitions must be removed from M to yield a model M ′ of η Thus, we can use any SAT solver to repair Kripke structures. Using a complete SAT solver yields a complete algorithm: it always finds a repair if one exists. We also show that CTL model repair is NP-complete. We extend the basic repair method in three directions: (1) the use of abstraction mappings, that is, repair a structure abstracted from M and then concretize the resulting repair to obtain a repair of M , (2) repair concurrent Kripke structures and concurrent programs: we use the pairwise method of Attie and Emerson to represent and repair the behavior of a concurrent program, as a set of “concurrent Kripke structures”, with only a quadratic increase in the size of the repair formula, and (3) repair hierarchical Kripke structures: we use a CTL formula to summarize the behavior of each “box,” and CTL deduction to relate the box formula with the overall specification.

We consider the subtractive model repair problem: given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M' that satisfies η. Thus, M can be repaired to satisfy η by deleting states and/or transitions. We give a reduction to boolean satisfiability, and implement the repair method using this reduction. We also extend the basic repair method in three directions: (1) the use of abstraction, and (2) the repair of concurrent Kripke structures and concurrent programs, and (3) the repair of hierarchical Kripke structures. These last two extensions both avoid state-explosion.