arXiv subjects

Samuel Judson

Publications and source records attributed to Samuel Judson.

4 recordsLinked to original sources

arXiv2026

BlindMarket: Enabling Verifiable, Confidential, and Traceable IP Core Distribution in Zero-Trust Settings

We present BlindMarket, an end-to-end zero-trust distribution framework for hardware IP cores. BlindMarket allows two parties, the IP user and the IP vendor, to complete an IP trading process with strong guarantees of verifiability and confidentiality before the transaction, and then traceability after. We propose verification heuristics and adapt the cone of influence-based design pruning to overcome the limited scalability common to cryptographic protocols and the hardness of the underlying hardware verification. We systematically evaluate our framework on a diverse set of real-world hardware benchmarks, and the results demonstrate that BlindMarket effectively completes across a diverse set of real-world hardware IP cores, demonstrating successful verification on 12 out of 13 designs and substantial performance improvements enabled by design pruning and control-flow guided heuristics.

cs.CR↗

arXiv2023

Analyzing Intentional Behavior in Autonomous Agents under Uncertainty

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.

cs.AI↗

arXiv2023

'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions

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 model accountability processes, such as trials or review boards, as Counterfactual-Guided Logic Exploration and Abstraction Refinement (CLEAR) loops. We use the formal methods of symbolic execution and satisfiability modulo theories (SMT) solving to discharge queries about agent behavior in factual and counterfactual scenarios, as adaptively formulated by a human investigator. In order to do so, for a decision algorithm $\mathcal{A}$ we use symbolic execution to represent its logic as a statement $\Pi$ in the decidable theory $\texttt{QF_FPBV}$. We implement our framework and demonstrate its utility on an illustrative car crash scenario.

cs.LO↗

arXiv2022

On Heuristic Models, Assumptions, and Parameters

Insightful interdisciplinary collaboration is essential to the principled governance of technology. When such efforts address the interaction between computation and society, they often focus on modeling, the process by which computer scientists formally define problems in order to enable algorithmic solutions. But modeling is a multifaceted and inherently imperfect process. Especially in interdisciplinary work, it often receives uneven scrutiny because of the practical challenges of communicating complex technical details to non-experts. We argue that there is an underappreciated if loose family of obscure and opaque technical caveats, choices, and qualifiers that the social effects of computing can depend just as much on as far more heavily scrutinized modeling choices. These artifacts are often used by researchers to paper over the incomplete theoretical foundations of computing or to burden shift responsibility for the impact of normative design decisions. Further, their nuanced technical nature often complicates thorough sociotechnical scrutiny of the discretionary decisions made to manage them. We describe three specific classes of such objects: heuristic models, assumptions, and parameters. We raise six reasons these objects may be hazardous to comprehensive analysis of computing and argue they deserve deliberate consideration as researchers explain scientific work.

cs.CY↗