How to Delegate Computations: The Power of No-Signaling Proofs

We construct a 1-round delegation scheme (i.e., argument-system) for every language computable in time t = t ( n ), where the running time of the prover is poly ( t ) and the running time of the verifier is n · polylog ( t ). In particular, for every language in P we obtain a delegation scheme with almost linear time verification. Our construction relies on the existence of a computational sub-exponentially secure private information retrieval ( PIR ) scheme. The proof exploits a curious connection between the problem of computation delegation and the model of multi-prover interactive proofs that are sound against no-signaling (cheating) strategies , a model that was studied in the context of multi-prover interactive proofs with provers that share quantum entanglement, and is motivated by the physical principle that information cannot travel faster than light. For any language computable in time t = t ( n ), we construct a multi-prover interactive proof ( MIP ), that is, sound against no-signaling strategies, where the running time of the provers is poly ( t ), the number of provers is polylog ( t ), and the running time of the verifier is n · polylog ( t ). In particular, this shows that the class of languages that have polynomial-time MIP s that are sound against no-signaling strategies, is exactly EXP . Previously, this class was only known to contain PSPACE . To convert our MIP into a 1-round delegation scheme, we use the method suggested by Aiello et al. (ICALP, 2000), which makes use of a PIR scheme. This method lacked a proof of security. We prove that this method is secure assuming the underlying MIP is secure against no-signaling provers.

Provably Safe Artificial General Intelligence via Interactive Proofs

Methods are currently lacking to prove artificial general intelligence (AGI) safety. An AGI ‘hard takeoff’ is possible, in which first generation AGI1 rapidly triggers a succession of more powerful AGIn that differ dramatically in their computational capabilities (AGIn << AGIn+1). No proof exists that AGI will benefit humans or of a sound value-alignment method. Numerous paths toward human extinction or subjugation have been identified. We suggest that probabilistic proof methods are the fundamental paradigm for proving safety and value-alignment between disparately powerful autonomous agents. Interactive proof systems (IPS) describe mathematical communication protocols wherein a Verifier queries a computationally more powerful Prover and reduces the probability of the Prover deceiving the Verifier to any specified low probability (e.g., 2−100). IPS procedures can test AGI behavior control systems that incorporate hard-coded ethics or value-learning methods. Mapping the axioms and transformation rules of a behavior control system to a finite set of prime numbers allows validation of ‘safe’ behavior via IPS number-theoretic methods. Many other representations are needed for proving various AGI properties. Multi-prover IPS, program-checking IPS, and probabilistically checkable proofs further extend the paradigm. In toto, IPS provides a way to reduce AGIn ↔ AGIn+1 interaction hazards to an acceptably low level.

Provably Safe Artificial General Intelligence via Interactive Proofs

Methods are currently lacking to prove artificial general intelligence (AGI) safety. An AGI &lsquo;hard takeoff&rsquo; is possible, in which first generation AGI1 rapidly triggers a succession of more powerful AGIn that differ dramatically in their computational capabilities (AGIn≪AGIn+1). No proof exists that AGI will benefit humans or of a sound value-alignment method. Numerous paths toward human extinction or subjugation have been identified. We suggest that probabilistic proof methods are the fundamental paradigm for proving safety and value-alignment between disparately powerful autonomous agents. Interactive proof systems (IPS) describe mathematical communication protocols wherein a Verifier queries a computationally more powerful Prover and reduces the probability of the Prover deceiving the Verifier to any specified low probability (e.g., 2-100). IPS procedures can test AGI behavior control systems that incorporate hard-coded ethics or value-learning methods. Mapping the axioms and transformation rules of a behavior control system to a finite set of prime numbers allows validation of &lsquo;safe&rsquo; behavior via IPS number-theoretic methods. Many other representations are needed for proving various AGI properties. Multi-prover IPS, program-checking IPS, and probabilistically checkable proofs further extend the paradigm. In toto, IPS provides a way to reduce AGIn&harr;AGIn+1 interaction hazards to an acceptably low level.

Steel: proof-oriented programming in a dependently typed concurrent separation logic

Steel is a language for developing and proving concurrent programs embedded in F ⋆ , a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F ⋆ , our work focuses on exposing the proof rules of the logic in a form that enables programs and proofs to be effectively co-developed. Our main contributions include a new formulation of a Hoare logic of quintuples involving both separation logic and first-order logic, enabling efficient verification condition (VC) generation and proof discharge using a combination of tactics and SMT solving. We relate the VCs produced by our quintuple system to solving a system of associativity-commutativity (AC) unification constraints and develop tactics to (partially) solve these constraints using AC-matching modulo SMT-dischargeable equations. Our system is fully mechanized and implemented in F ⋆ . We evaluate it by developing several verified programs and libraries, including various sequential and concurrent linked data structures, proof libraries, and a library for 2-party session types. Our experience leads us to conclude that our system enables a mixture of automated and interactive proof, making it productive to build programs foundationally verified against a highly expressive, state-of-the-art CSL.

Fast Mutual Authentication Using RSA Moduli

We describe a fast three-round mutual authentication protocol for parties A and B belonging to the same coalition group. Parties A and B keep their own independent long-term private keys that are used in the process of authentication and can be used for other purposes. The scheme assumes an initial setup with a trusted third party T. This party initiates another secret information that includes factors of a large RSA modulus. For authentication, both parties must demonstrate each other the knowledge of their private keys without revealing them and the ability to factorize a large RSA modulus. Thus, the protocol based on the suggested scheme provides reciprocal authentication. The scheme possesses all desirable properties of an interactive proof, i.e., completeness, soundness, and zero-knowledge. The security of the protocol relies on assumptions of difficulty of the RSA factorization and existence of a cryptographic hash function.

Fast Mutual Authentication Using RSA Moduli

We describe a fast three-round mutual authentication protocol for parties A and B belonging to the same coalition group. Parties A and B keep their own independent long-term private keys that are used in the process of authentication and can be used for other purposes. The scheme assumes an initial setup with a trusted third party T. This party initiates another secret information that includes factors of a large RSA modulus. For authentication, both parties must demonstrate each other the knowledge of their private keys without revealing them and the ability to factorize a large RSA modulus. Thus, the protocol based on the suggested scheme provides reciprocal authentication. The scheme possesses all desirable properties of an interactive proof, i.e., completeness, soundness, and zero-knowledge. The security of the protocol relies on assumptions of difficulty of the RSA factorization and existence of a cryptographic hash function.

Asymmetric cryptographic protocols with a blockchain core: development problems and their solutions

The problem of axiomatic construction of secure cryptographic protocols is closely related to the choice of basic cryptographic blocks from which a cryptographic protocol of arbitrary complexity can be built. Let’s call such blocks primitive cryptographic protocols. Along with a traditional choice as primitive secret sharing protocols and non-interactive proof protocols today blockchain is considered to be a primitive cryptographic protocol. The security of such cryptographic protocols with a blockchain core is studied a bit today. We consider the methods for increasing the security of protocols with blockchain core by using a new agreement protocol in the blockchain, which is secure in the information theoretically sense.

CoCEC: An Automatic Combinational Circuit Equivalence Checker Based on the Interactive Theorem Prover

Checking the equivalence of two Boolean functions, or combinational circuits modeled as Boolean functions, is often desired when reliable and correct hardware components are required. The most common approaches to equivalence checking are based on simulation and model checking, which are constrained due to the popular memory and state explosion problems. Furthermore, such tools are often not user-friendly, thereby making it tedious to check the equivalence of large formulas or circuits. An alternative is to use mathematical tools, called interactive theorem provers, to prove the equivalence of two circuits; however, this requires human effort and expertise to write multiple output functions and carry out interactive proof of their equivalence. In this paper, we (1) define two simple, one formal and the other informal, gate-level hardware description languages, (2) design and develop a formal automatic combinational circuit equivalence checker (CoCEC) tool, and (3) test and evaluate our tool. The tool CoCEC is based on human-assisted theorem prover Coq, yet it checks the equivalence of circuit descriptions purely automatically through a human-friendly user interface. It either returns a machine-readable proof (term) of circuits’ equivalence or a counterexample of their inequality. The interface enables users to enter or load two circuit descriptions written in an easy and natural style. It automatically proves, in few seconds, the equivalence of circuits with as many as 45 variables (3.5 × 10 13 states). CoCEC has a mathematical foundation, and it is reliable, quick, and easy to use. The tool is intended to be used by digital logic circuit designers, logicians, students, and faculty during the digital logic design course.

owards a quantum-inspired proof for IP = PSPACE

We explore quantum-inspired interactive proof systems where the prover is limited. Namely, we improve on a result by \cite{AG17} showing a quantum-inspired interactive protocol ($\IP$) for $PreciseBQP$ where the prover is only assumed to be a $\PreciseBQP$ machine, and show that the result can be strengthened to show an $\IP$ for $\NP^{\PP}$ with a prover which is only assumed to be an $\NP^{\PP}$ machine - which was not known before. We also show how the protocol can be used to directly verify $\QMA$ computations, thus connecting the sum-check protocol by \cite{AAV13} with the result of \cite{AG17,LFKN90}. Our results shed light on a quantum-inspired proof for $\IP=\PSPACE$, as $\PreciseQMA$ captures the full $\PSPACE$ power.

Verified secure compilation for mixed-sensitivity concurrent programs

Proving only over source code that programs do not leak sensitive data leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. Furthermore, software does not always have the luxury of limiting itself to single-threaded computation with resources statically dedicated to each user to ensure the confidentiality of their data. This results in mixed-sensitivity concurrent programs, which might reuse memory shared between their threads to hold data of different sensitivity levels at different times; for such programs, a compiler must preserve the value-dependent coordination of such mixed-sensitivity reuse despite the impact of concurrency. Here we demonstrate, using Isabelle/HOL, that it is feasible to verify that a compiler preserves noninterference, the strictest kind of confidentiality property, for mixed-sensitivity concurrent programs. First, we present notions of refinement that preserve a concurrent value-dependent notion of noninterference that we have designed to support such programs. As proving noninterference-preserving refinement can be considerably more complex than the standard refinements typically used to verify semantics-preserving compilation, our notions include a decomposition principle that separates the semantics preservation from security preservation concerns. Second, we demonstrate that these refinement notions are applicable to verified secure compilation, by exercising them on a single-pass compiler for mixed-sensitivity concurrent programs that synchronise using mutex locks, from a generic imperative language to a generic RISC-style assembly language. Finally, we execute our compiler on a non-trivial mixed-sensitivity concurrent program modelling a real-world use case, thus preserving its source-level noninterference properties down to an assembly-level model automatically. All results are formalised and proved in the Isabelle/HOL interactive proof assistant. Our work paves the way for more fully featured compilers to offer verified secure compilation support to developers of multithreaded software that must handle data of multiple sensitivity levels.