Abstract We present $$\textsf{soid}$$ soid , a tool for interrogating the decision making of autonomous agents using SMT-based automated reasoning. Relying on the Z3 SMT solver and KLEE symbolic execution engine, $$\textsf{soid}$$ soid allows investigators to receive rigorously proven answers to factual and counterfactual queries about agent behavior, enabling effective legal and engineering accountability for harmful or otherwise incorrect decisions. We evaluate $$\textsf{soid}$$ soid qualitatively and quantitatively on a pair of examples, i) a buggy implementation of a classic decision tree inference benchmark from the explainable AI (XAI) literature; and ii) a car crash in a simulated physics environment. For the latter, we also contribute the $$\textsf{soid}\hbox {-}\!\textsf{gui}$$ soid - gui , a domain-specific, web-based example interface for legal and other practitioners to specify factual and counterfactual queries without requiring sophisticated programming or formal methods expertise.

Due to the globalization of the semiconductor supply chain, chip fabrication now involves multiple parties, including intellectual property (IP) vendors and Electronic Design Automation (EDA) tool vendors. Involving multiple entities and valuable IP naturally raises security and privacy concerns. Various frameworks and tools, such as the IEEE 1735 standard for IP protection, have been developed to mitigate the risk of theft. However, existing solutions fail to address all the threats envisioned by the zero-trust model. We propose a novel zero-trust formal verification framework that requires only two essential parties: IP users and IP vendors. This framework leverages secure multiparty computation to ensure the security and privacy of the hardware verification process. Our proposed solution allows IP users and IP vendors to independently convert the hardware design and assertions into conjunctive normal form (CNF), and then apply privacy-preserving SAT solving to verify the conformance of the design to the specification. This paper introduces a domain-specific secure decision procedure, hw-ppSAT, designed to overcome the scalability challenges of using SAT solving in hardware design verification. Our approach also leverages property-based hardware optimizations and domain-specific heuristics to enhance the verification process. We showcase the framework's effectiveness through its application to several open-source benchmarks.

A zero-knowledge proof (ZKP) is a powerful cryptographic primitive used in many decentralized or privacy-focused applications. However, the high overhead of ZKPs can restrict their practical applicability. We design a programming language, Ou, aimed at easing the programmer's burden when writing efficient ZKPs, and a compiler framework, Lian, that automates the analysis and distribution of statements to a computing cluster. Ou uses programming language semantics, formal methods, and combinatorial optimization to automatically partition an Ou program into efficiently sized chunks for parallel ZK-proving and/or verification. We contribute: (1) A front-end language where users can write proof statements as imperative programs in a familiar syntax; (2) A compiler architecture and implementation that automatically analyzes the program and compiles it into an optimized IR that can be lifted to a variety of ZKP constructions; and (3) A cutting algorithm, based on Pseudo-Boolean optimization and Integer Linear Programming, that reorders instructions and then partitions the program into efficiently sized chunks for parallel evaluation and efficient state reconciliation.

Principled accountability for autonomous decision-making in uncertain environments requires distinguishing intentional outcomes from negligent designs from actual accidents. We propose analyzing the behavior of autonomous agents through a quantitative measure of the evidence of intentional behavior. We model an uncertain environment as a Markov Decision Process (MDP). For a given scenario, we rely on probabilistic model checking to compute the ability of the agent to influence reaching a certain event. We call this the scope of agency. We say that there is evidence of intentional behavior if the scope of agency is high and the decisions of the agent are close to being optimal for reaching the event. Our method applies counterfactual reasoning to automatically generate relevant scenarios that can be analyzed to increase the confidence of our assessment. In a case study, we show how our method can distinguish between 'intentional' and 'accidental' traffic collisions.