Date of Award
Spring 2024
Document Type
Dissertation
Degree Name
Doctor of Philosophy (PhD)
Department
Computer Science
First Advisor
Piskac, Ruzica
Abstract
The increasing complexity of software systems presents a growing challenge to the societal and legal governance of modern technology. Understanding how algorithmic decisions are made and how private, proprietary, or otherwise legally-encumbered data is generated and consumed is essential to the design of robust and accountable computing. This dissertation contributes algorithmic techniques based on formal methods for program analysis and verification -- and at times combined with cryptographic constructions for privacy-preserving computation -- that are designed with the goal of supporting the principled and effective governance of software and cyberphysical systems. First, this dissertation investigates how Satisfiability Modulo Theories (SMT)-based formal methods can enable adaptive, interactive querying of factual and counterfactual agent behavior in a manner consistent with existing legal theory and practice. Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal theory offers a paramount method for assessing culpability: putting the agent `on the stand' to subject their actions and intentions to cross-examination. We show that under minimal assumptions automated reasoning can rigorously interrogate algorithmic behaviors as in the adversarial process of legal fact finding. We use the formal methods of symbolic execution and SMT solving to discharge queries about agent behavior in factual and counterfactual scenarios, as adaptively formulated by a human investigator. Second, this dissertation considers how to reconcile program verification with privacy and propriety constraints about code and data through the use of applied cryptography. We raise a decision procedure for the model checking of temporal logics -- a cornerstone approach to program verification widely applied in both research and industry -- into a cryptographic protocol through the use of secure multiparty computation (MPC). Our protocol enables two mutually distrustful parties, the program developer and the auditor, to check whether the developer's model meets the auditor's specification without disclosing either input to the other party. One potential application is to controlled distributed app stores, where an auditor can put code through rigorous formalized analysis without gaining direct access to competitor's software in a manner that could be abused in furtherance of monopolistic practices. Third, this dissertation raises concern about a pattern apparent in technical research, in which both caveats to correctness and difficult design decisions relevant to the societal impact of a technology are foisted onto practitioners through the use of poorly understood and communicated heuristic models, assumptions, and parameters. We chart the course of this pattern through its use in diverse fields including cryptography, privacy, artificial intelligence, and formal methods research, and consider potential directions for technologists to more effectively communicate the implications of computer science research to governance practitioners.
Recommended Citation
Judson, Samuel, "(Private) Formal Methods for Rigorously Governable Systems" (2024). Yale Graduate School of Arts and Sciences Dissertations. 1432.
https://elischolar.library.yale.edu/gsas_dissertations/1432
