arXiv subjects

James Parker

Publications and source records attributed to James Parker.

12 recordsLinked to original sources

arXiv2026

Automating Bitvector and Finite Field Equivalence Proofs in Lean

Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows are either manual or rely on SMT solvers, which scale poorly on some classes of problems for reasons that include difficulties with conversion operators and challenges reasoning about inequalities. To address these limitations, we present a novel Lean tactic BitModEq that leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors. Our approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.

cs.LO↗

arXiv2023

Cheesecloth: Zero-Knowledge Proofs of Real-World Vulnerabilities

Currently, when a security analyst discovers a vulnerability in critical software system, they must navigate a fraught dilemma: immediately disclosing the vulnerability to the public could harm the system's users; whereas disclosing the vulnerability only to the software's vendor lets the vendor disregard or deprioritize the security risk, to the detriment of unwittingly-affected users. A compelling recent line of work aims to resolve this by using Zero Knowledge (ZK) protocols that let analysts prove that they know a vulnerability in a program, without revealing the details of the vulnerability or the inputs that exploit it. In principle, this could be achieved by generic ZK techniques. In practice, ZK vulnerability proofs to date have been restricted in scope and expressibility, due to challenges related to generating proof statements that model real-world software at scale and to directly formulating violated properties. This paper presents CHEESECLOTH, a novel proofstatement compiler, which proves practical vulnerabilities in ZK by soundly-but-aggressively preprocessing programs on public inputs, selectively revealing information about executed control segments, and formalizing information leakage using a novel storage-labeling scheme. CHEESECLOTH's practicality is demonstrated by generating ZK proofs of well-known vulnerabilities in (previous versions of) critical software, including the Heartbleed information leakage in OpenSSL and a memory vulnerability in the FFmpeg graphics framework.

cs.CR↗

arXiv2022

ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification

Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is often needed in realistic applications but breaks non-interference. We present ANOSY, an approximate knowledge synthesizer for quantitative declassification policies. ANOSY uses refinement types to automatically construct machine checked over- and under-approximations of attacker knowledge for boolean queries on multi-integer secrets. It also provides an AnosyT monad to track the attacker knowledge over multiple declassification queries and checks for violations against user-specified policies in information flow control applications. We implement a prototype of ANOSY and show that it is precise and permissive: up to 14 declassification queries are permitted before a policy violation occurs using the powerset of intervals domain.

cs.PL↗

arXiv2021

Balboa: Bobbing and Weaving around Network Censorship

We introduce Balboa, a link obfuscation framework for censorship circumvention. Balboa provides a general framework for tunneling data through existing applications. Balboa sits between an application and the operating system, intercepting outgoing network traffic and rewriting it to embed data. To avoid introducing any distinguishable divergence from the expected application behavior, Balboa only rewrites traffic that matches an externally specified \emph{traffic model} pre-shared between the communicating parties. The traffic model captures some subset of the network traffic (e.g., some subset of music an audio streaming server streams). The sender uses this model to replace outgoing data with a pointer to the associated location in the model and embed data in the freed up space. The receiver then extracts the data, replacing the pointer with the original data from the model before passing the data on to the application. When using TLS, this approach means that application behavior with Balboa is \emph{equivalent}, modulo small (protocol-dependent) timing differences, to if the application was running without Balboa. Balboa differs from prior approaches in that it (1) provides a framework for tunneling data through arbitrary (TLS-protected) protocols/applications, and (2) runs the unaltered application binaries on standard inputs, as opposed to most prior tunneling approaches which run the application on non-standard -- and thus potentially distinguishable -- inputs. We present two instantiations of Balboa -- one for audio streaming and one for web browsing -- and demonstrate the difficulty of identifying Balboa by a machine learning classifier.

cs.CR↗

arXiv2020

The Completed SDSS-IV extended Baryon Oscillation Spectroscopic Survey: Baryon acoustic oscillations with Lyman-$α$ forests

We present a measurement of baryonic acoustic oscillations (BAO) from Lyman-$α$ (Ly$α$) absorption and quasars at an effective redshift $z=2.33$ using the complete extended Baryonic Oscillation Spectroscopic Survey (eBOSS). The sixteenth and final eBOSS data release (SDSS DR16) contains all data from eBOSS and its predecessor, the Baryonic Oscillation Spectroscopic Survey (BOSS), providing $210,005$ quasars with $z_{q}>2.10$ that are used to measure Ly$α$ absorption. We measure the BAO scale both in the auto-correlation of Ly$α$ absorption and in its cross correlation with $341,468$ quasars with redshift $z_{q}>1.77$. Apart from the statistical gain from new quasars and deeper observations, the main improvements over previous work come from more accurate modeling of physical and instrumental correlations and the use of new sets of mock data. Combining the BAO measurement from the auto- and cross-correlation yields the constraints of the two ratios $D_{H}(z=2.33)/r_{d} = 8.99 \pm 0.19$ and $D_{M}(z=2.33)/r_{d} = 37.5 \pm 1.1$, where the error bars are statistical. These results are within $1.5σ$ of the prediction of the flat-$Λ$CDM cosmology of Planck~(2016). The analysis code, \texttt{picca}, the catalog of the flux-transmission field measurements, and the $Δχ^{2}$ surfaces are publicly available.

astro-ph.CO↗

arXiv2020

Volatile Sample Return in the Solar System

We advocate for the realization of volatile sample return from various destinations including: small bodies, the Moon, Mars, ocean worlds/satellites, and plumes. As part of recent mission studies (e.g., Comet Astrobiology Exploration SAmple Return (CAESAR) and Mars Sample Return), new concepts, technologies, and protocols have been considered for specific environments and cost. Here we provide a plan for volatile sample collection and identify the associated challenges with the environment, transit/storage, Earth re-entry, and curation. Laboratory and theoretical simulations are proposed to verify sample integrity during each mission phase. Sample collection mechanisms are evaluated for a given environment with consideration for alteration. Transport and curation are essential for sample return to maximize the science investment and ensure pristine samples for analysis upon return and after years of preservation. All aspects of a volatile sample return mission are driven by the science motivation: isotope fractionation, noble gases, organics and prebiotic species; plus planetary protection considerations for collection and for the sample. The science value of sample return missions has been clearly demonstrated by previous sample return programs and missions. Sample return of volatile material is key to understanding (exo)planet formation, evolution, and habitability. Returning planetary volatiles poses unique and potentially severe technical challenges. These include preventing changes to samples between (and including) collection and analyses, and meeting planetary protection requirements.

astro-ph.IM↗

arXiv2019

Build It, Break It, Fix It: Contesting Secure Development

Typical security contests focus on breaking or mitigating the impact of buggy systems. We present the Build-it, Break-it, Fix-it (BIBIFI) contest, which aims to assess the ability to securely build software, not just break it. In BIBIFI, teams build specified software with the goal of maximizing correctness, performance, and security. The latter is tested when teams attempt to break other teams' submissions. Winners are chosen from among the best builders and the best breakers. BIBIFI was designed to be open-ended; teams can use any language, tool, process, etc. that they like. As such, contest outcomes shed light on factors that correlate with successfully building secure software and breaking insecure software. We ran three contests involving a total of 156 teams and three different programming problems. Quantitative analysis from these contests found that the most efficient build-it submissions used C/C++, but submissions coded in a statically-type safe language were 11 times less likely to have a security flaw than C/C++ submissions. Break-it teams that were also successful build-it teams were significantly better at finding security bugs.

cs.CR↗

arXiv2019

LWeb: Information Flow Security for Multi-tier Web Applications

This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enforcement library with the Yesod web programming framework. The implementation has two parts. First, we extract the core of LIO into a monad transformer (LMonad) and then apply it to Yesod's core monad. Second, we extend Yesod's table definition DSL and query functionality to permit defining and enforcing label-based policies on tables and enforcing them during query processing. LWeb's policy language is expressive, permitting dynamic per-table and per-row policies. We formalize the essence of LWeb in the $λ_{LWeb}$ calculus and mechanize the proof of noninterference in Liquid Haskell. This mechanization constitutes the first metatheoretic proof carried out in Liquid Haskell. We also used LWeb to build a substantial web site hosting the Build it, Break it, Fix it security-oriented programming contest. The site involves 40 data tables and sophisticated policies. Compared to manually checking security policies, LWeb imposes a modest runtime overhead of between 2% to 21%. It reduces the trusted code base from the whole application to just 1% of the application code, and 21% of the code overall (when counting LWeb too).

cs.PL↗

arXiv2016

Build It, Break It, Fix It: Contesting Secure Development

Typical security contests focus on breaking or mitigating the impact of buggy systems. We present the Build-it Break-it Fix-it BIBIFI contest which aims to assess the ability to securely build software not just break it. In BIBIFI teams build specified software with the goal of maximizing correctness performance and security. The latter is tested when teams attempt to break other teams submissions. Winners are chosen from among the best builders and the best breakers. BIBIFI was designed to be open-ended - teams can use any language tool process etc. that they like. As such contest outcomes shed light on factors that correlate with successfully building secure software and breaking insecure software. During we ran three contests involving a total of teams and two different programming problems. Quantitative analysis from these contests found that the most efficient build-it submissions used CC but submissions coded in a statically-typed language were less likely to have a security flaw build-it teams with diverse programming-language knowledge also produced more secure code. Shorter programs correlated with better scores. Break-it teams that were also build-it teams were significantly better at finding security bugs.

cs.CR↗

arXiv2013

4D, N=1 Supergravity Genomics

The off-shell representation theory of 4D, $\mathcal{N}=1$ supermultiplets can be categorized in terms of distinct irreducible graphical representations called adinkras as part of a larger effort we call supersymmetry `genomics.' Recent evidence has emerged pointing to the existence of three such fundamental adinkras associated with distinct equivalence classes of a Coxeter group. A partial description of these adinkras is given in terms of two types, termed cis-and trans-adinkras (the latter being a degenerate doublet) in analogy to cis/trans isomers in chemistry. Through a new and simple procedure that uses adinkras, we find the irreducible off-shell adinkra representations of 4D, $\mathcal{N}=1$ supergravity, in the old-minimal, non-minimal, and conformal formulations. This procedure uncovers what appears to be a selection rule useful to reverse engineer adinkras to higher dimensions. We categorize the supergravity representations in terms of the number of cis-($n_c$) and trans-($n_t$) adinkras in the representation and synthesize our new results with our previous supersymmetry genomics results into a group theoretic framework.

hep-th↗

arXiv2012

4D, N = 1 Supersymmetry Genomics (II)

We continue the development of a theory of off-shell supersymmetric representations analogous to that of compact Lie algebras such as SU(3). For off-shell 4D, N = 1 systems, quark-like representations have been identified [1] in terms of cis-Adinkras and trans-Adinkras and it has been conjectured that arbitrary representations are composites of $n_c$-cis and $n_t$-trans representations. Analyzing the real scalar and complex linear superfield multiplets, these "chemical enantiomer" numbers are found to be $n_c$ = $n_t$ = 1 and $n_c$ = 1, $n_t$ = 2, respectively.

hep-th↗

arXiv2011

A Detailed Investigation of First and Second Order Supersymmetries for Off-Shell N = 2 and N = 4 Supermultiplets

This paper investigates the d = 4, N = 4 Abelian, global Super-Yang Mills system (SUSY-YM). It is shown how the N = 2 Fayet Hypermultiplet (FH) and N = 2 vector multiplet (VM) are embedded within. The central charges provide a plethora of information as to further symmetries of the Lagrangian. Several of these symmetries are calculated to second order. It is hoped that investigations such as these may yield avenues to help solve the auxiliary field closure problem for d = 4, N = 4, SUSY-YM and the d = 4, N = 2 Fayet-Hypermultiplet, without using an infinite number of auxiliary fields.

hep-th↗