Eli Ben‐Sasson, Alessandro Chiesa, Michael A. Forbes, Ariel Gabizon · 6 authors
We study the problem of constructing proof systems that achieve both soundness and zero knowledge unconditionally (without relying on intractability assumptions). Known techniques for this goal are primarily combinatorial, despite the fact that constructions of interactive proofs (IPs) and probabilistically checkable proofs (PCPs) heavily rely on algebraic techniques to achieve their properties.
This work reports on the experience arising from the master internship contract-based design tailored to safety issues for cyber-physical systems (CPS). The main educational goal is to confront the student with realistic mixed-critical smart CPS systems, using the railway domain and autonomous trains as a case study. The results show that, for this class of systems, education should transition from a 2D to a 3D modeling design space, which is much better suited to visualizing the evolution and the underlying properties of the system. We use contract-based design to properly deal with the integration and composition of heterogeneous components, where safety aspects require special attention. The main scientific and technical results concern the implementation of contract-based design in a 3D tool. Finally, we discuss the teaching methodology underlying the internship and the competences required to address the design of a (critical) CPS by the new generation of students.
The realization of large and complex cyber-physical systems (such as "smart" transportation, energy, security, and health-care systems) is creating design and verification challenges which will soon become insurmountable with the current engineering practices. These highly heterogeneous systems, tightly combining physical processes with computation, communication, and control elements, would substantially benefit from hierarchical and compositional methodologies to make their design possible let alone optimal. Several languages and tools have been proposed over the years to enable model-based development of complex systems. However, an all-encompassing design framework that helps interconnect different tools, possibly operating on different system representations, is still missing.In this dissertation, we introduce a design methodology that addresses the complexity and heterogeneity of cyber-physical systems by using assume-guarantee contracts to formalize the design process and enable the realization of system architectures and control algorithms in a hierarchical and compositional way. In our methodology, components are specified by contracts, and systems by compositions of contracts. Contracts explicitly define the assumptions of a component on its environment and the guarantees of the component under these assumptions. Contract operations and relations, such as composition, conjunction and refinement allow proving that: (i) an aggregation of components are compatible, i.e. there exists a legal environment in which they can operate; (ii) a set of specifications are consistent, i.e. there exists an implementation satisfying all of them; (iii) an aggregation of components refines a specification, i.e. it implements the specification contract and is able to operate in any environment admitted by it. While horizontal contracts are used to specify components and aggregations of components at the same level of abstraction, we introduce the notion of vertical contracts to reason about richer refinement relations and mappings between different abstraction levels, possibly described by heterogeneous architectures and behavior formalisms. Moreover, we further investigate the problem of compatibility for systems with uncontrolled inputs and controlled outputs, by establishing a link between the theory of contracts and the one of interfaces, which rely on different mathematical formalisms, while sharing the same objectives. From this link, we derive a new projection operator on contracts that enables the preservation of the semantics of interface composition and compatibility.Resting on the above contract framework, the design is carried out as a sequence of refinement steps from a high-level specification to an implementation built out of a library of components at the lower level. To allow for requirement analysis and early detection of inconsistencies, top-level system requirements are captured as contracts, by leveraging a front-end pattern-based specification language and a set of back-end formal languages, including mixed integer-linear constraints and temporal logic. Top-level contracts are then refined to achieve independent development of system architectures and control algorithms, by combining synthesis from requirements and optimization methods.To enable efficient architecture selection under safety and reliability constraints, we explore two optimization-based methods that use an approximate reliability analysis technique to overcome the exponential complexity of exact computations. The Integer-Linear Programming with Approximate Reliability (ILP-AR) method generates larger, monolithic optimization problems using approximate but efficient reliability computations with an explicit theoretical bound on the error. Conversely, the Integer-Linear Programming Modulo Reliability (ILP-MR) method breaks the complex architecture selection task into a sequence of smaller optimization tasks without reliability constraints, interleaved with exact reliability checks. By relying on efficient mechanisms to prune out candidate architectures that are inconsistent with the reliability constraints, ILP-MR can run faster than ILP-AR on large problem instances.We further explore two methods to systematically design control strategies for a given architecture. The reactive synthesis-based optimal control mapping (RS-OCM) method generates controllers by combining reactive synthesis from linear temporal logic contracts with optimization techniques based on simulation and monitoring of signal temporal logic contracts. Different design concerns are then addressed by leveraging the most appropriate abstraction levels, using contracts from the pre-characterized library to accelerate verification tasks. The programming-based optimal control mapping (P-OCM) method uses, instead, a discrete-time representation of the system and a formalization of the design requirements in terms of arithmetic constraints over real numbers to cast the control problem as an optimization problem over a finite time horizon. The optimization problem is then solved with a receding horizon approach and scales better than monolithic reactive synthesis from linear temporal logic.We demonstrate, for the first time, the effectiveness of a contract-based design flow on real-life examples of industrial relevance, namely, the design of aircraft electric power distribution and environment control systems. In our framework, optimal selection of large, industrial-scale power system architectures can be performed in a few minutes. Design validation of power system controllers based on linear temporal logic contracts shows up to two orders of magnitude improvement in terms of execution time with respect to conventional techniques. Finally, our optimization-based load management scheme allows better resource utilization than a conventional one.
Marcin Andrychowicz, Stefan Dziembowski, Daniel Malinowski, Łukasz Mazurek
Bitcoin is a peer-to-peer cryptographic currency system. Since its introduction in 2008, Bitcoin has gained noticeable popularity, mostly due to its following properties: (1) the transaction fees are very low, and (2) it is not controlled by any central authority, which in particular means that nobody can "print" the money to generate inflation. Moreover, the transaction syntax allows to create the so-called contracts, where a number of mutually-distrusting parties engage in a protocol to jointly perform some financial task, and the fairness of this process is guaranteed by the properties of Bitcoin. Although the Bitcoin contracts have several potential applications in the digital economy, so far they have not been widely used in real life. This is partly due to the fact that they are cumbersome to create and analyze, and hence risky to use. In this paper we propose to remedy this problem by using the methods originally developed for the computer-aided analysis for hardware and software systems, in particular those based on the timed automata. More concretely, we propose a framework for modeling the Bitcoin contracts using the timed automata in the UPPAAL model checker. Our method is general and can be used to model several contracts. As a proof-of-concept we use this framework to model some of the Bitcoin contracts from our recent previous work. We then automatically verify their security in UPPAAL, finding (and correcting) some subtle errors that were difficult to spot by the manual analysis. We hope that our work can draw the attention of the researchers working on formal modeling to the problem of the Bitcoin contract verification, and spark off more research on this topic.
This technical report presents the design and implementation of a Vehicle Follow Control (VFC) func-tion. The main goal of the project focuses on the Proof-Of-Concept of the functional behavior by Rapid Control Prototyping. First, the problem was analyzed by making a feasibility analysis; taking into account the challenges involved, necessary tools, methods and technology available. Second a requirement elicitation process was carried out using the CAFCR method. The Product Creation Process (PCP) followed at the compa-ny was analyzed and used to obtain the customer wishes related to the function. In addition, the relevant stake-holders were identified and a context diagram was created to define the scope. Use case scenarios were proposed to obtain the desired functionality, which served as an input to formulate the VFC Sys-tem Requirements. Subsequently, the architecture for the design was proposed, where different software components were identified. The controller design consists of four major components: Supervisor con-troller, Governor, Splitter and Hill Holder. The Supervisor controller was designed based on the func-tional requirements, using the company’s heuristic approach to design state-flow charts. The Governor was designed using a combined distance/speed control approach. The design of the Splitter was carried out by splitting the control signals to the respective vehicle actuators. Finally, the design of the Hill Holder was performed using a state-flow chart and a vehicle model. This was done by estimating the amount of force needed to prevent the vehicle from moving when driving on a hill. The controller was designed using Matlab, and implemented in the prototype vehicle using dSPACE HW/SW. A radar target filter algorithm was designed to properly filter the data coming from the radar and to detect the target vehicle to follow. The Verification and Validation phase was carried out according to the V-cycle model. A series of test cases were run with the vehicle to assess whether the functionality meets the requirements, and whether it fulfills the customer wishes. It was concluded that the RCP platform created for this project provides an important contribution for the company, since it can be used for the integration with other functions involving longitudinal control, which is included in the road map for future autonomous driving.
The multi discrete logarithm problem and the zero-knowledge proolf protocol were proposed to efficiently solve the zero-knowledge proof of the roots of polynomials,based on the hardness of computing the discrete logarithms.In the protocol,the prover computes the discrete logarithms of each term of the polynomial and obtains A1,A2,…,An,which are sent to the verifier.Based on the value of(A1A2…An)modp,the verifier verifies the prover's ownership of the root.The protocol needs to be executed several rounds to reduce the possibility of cheating.Theoretical analyses show that the chance of successfully cheating decays exponentially with increasing number of rounds,so the protocol is secure and reliable.
The abstraction of cryptographic operations by term algebras, called Dolev–Yao models, is essential in almost all tool-supported methods for proving security protocols. Recently significant progress was made in proving that Dolev–Yao models offering the core cryptographic operations such as encrypt ion and digital signatures can be sound with respect to actual cryptographic realizations and security definitions. Recent work, however, has started to extend Dolev–Yao models to more sophisticated operations with unique security features. Zero-knowledge proofs arguably constitute the most amazing such extension. In this paper, we first identify which additional properties a cryptographic (non-interactive) zero-knowledge proof needs to fulfill in order to serve as a computationally sound implementation of symbolic (Dolev–Yao style) zero-knowledge proofs; this leads to the novel definition of a symbolically-sound zero-knowledge proof system. We prove that even in the presence of arbitrary active adversaries, such proof systems constitute computationally sound implementations of symbolic zero-knowledge proofs. This yields the first computational soundness result for symbolic zero-knowledge proofs and the first such result against fully active adversaries of Dolev–Yao models that go beyond the core cryptographic operations.
The purpose of this paper is to give four new applications of the Quillen-Suslin theorem to mathematical systems theory. Using a constructive version of the Quillen-Suslin theorem, also known as Serre's conjecture, we show how to effectively compute flat outputs and injective parametrizations of flat multidimensional linear systems. We prove that a flat multidimensional linear system is algebraically equivalent to the controllable 1-D dimensional linear systems obtained by setting all but one functional operator to zero in the polynomial matrix defining the system. In particular, we show that a flat ordinary differential time-delay linear system is algebraically equivalent to the corresponding ordinary differential system without delay, i.e., the controllable ordinary differential linear system obtained by setting all the delay amplitudes to zero. We also give a constructive proof of a generalization of Serre's conjecture known as Lin-Bose's conjecture. Moreover, we show how to constructively compute (weakly) left-/right-/doubly coprime factorizations of rational transfer matrices over a commutative polynomial ring. The Quillen-Suslin theorem also plays a central part in the so-called decomposition problem of linear functional systems studied in the literature of symbolic computation. In particular, we show how the basis computation of certain free modules, coming from projectors of the endomorphism ring of the module associated with the system, allows us to obtain unimodular matrices which transform the system matrix into an equivalent block-triangular or a block-diagonal form. Finally, we demonstrate the package QuillenSuslin which, to our knowledge, contains the first implementation of the Quillen-Suslin theorem in a computer algebra system as well as the different algorithms developed in the paper.
Open access
Advanced Differential Equations and Dynamical Systems
The thesis is about a breadth-first exploration of logical concepts in cryptography and their linguistic abstraction and model-theoretic combination in a comprehensive logical system, called CPL (for Cryptographic Protocol Logic ). We focus on two fundamental aspects of cryptography. Namely, the security of communication (as opposed to security of storage ) and cryptographic protocols (as opposed to cryptographic operators ). The logical concepts explored are the following. Primary concepts: the modal concepts of belief, knowledge, norms, provability, space, and time. Secondary concepts: belief with error control, individual and propositional knowledge, confidentiality norms, truth-functional and relevant (in particular, intuitionistic) implication, multiple and complex truth values, and program types. The distinguishing feature of CPL is that it unifies and refines a variety of existing approaches. This feature is the result of our wholistic conception of property-based (modal logics) and model-based (process algebra) formalisms. We illustrate the expressiveness of CPL on representative requirements engineering case studies. Further, we extend (core) CPL (qualitative time) with rational-valued time , i.e., time stamps, timed keys, and potentially drifting local clocks, to tCPL (quantitative time). Our extension is conservative and provides further evidence for Lamport's claim that adding real time to an untimed formalism is really simple. Furthermore, we sketch an extension of (core) CPL with a notion of probabilistic polynomial-time (PP) computation. We illustrate the expressiveness of this extended logic (ppCPL) on tentative formalisation case studies of fundamental and applied concepts. Fundamental concepts: (1) one-way function, (2) hard-core predicate, (3) computational indistinguishability, (4) ( n -party) interactive proof, and (5) ( n -prover) zero-knowledge. Applied concepts: (1) security of encryption schemes, (2) unforgeability of signature schemes, (3) attacks on encryption schemes, (4) attacks on signature schemes, and (5) breaks of signature schemes. In the light of logic, adding PP to a formalism for cryptographic protocols is perhaps also simple and can be achieved with an Ockham's razor extension of an existing core logic, namely CPL.
Formal systems Formal systems are kinds of mathematical games with strings of symbols and precise rules. They mimic the idea of a ‘proof’. This chapter introduces formal systems through an example that turns out to be closely connected with König's Lemma. This simple example is based on the trees that we studied earlier. Formal systems are the ‘arguments from limited knowledge’ that we talked about earlier, and working in them is like being the ant following a tree who cannot see beyond the immediate node it happens to be at. The particular system that we shall look at here will put some more detail on the ideas introduced earlier about ‘two ways of doing it’ and how they can be played off against each other to advantage. It is based on finite sequences, or strings, of 0s and 1s. The set of all such strings is denoted 2* or 2 <ω and, as we have seen, this set can be regarded as a full binary tree. We shall write the empty string of length zero as ⊥. Now consider a game starting from a subset ∑ ⊆ 2* with the following rules specifying when a string may be written down. (Given Strings Rule) You may write down any string σ in ∑. (Lengthening Rule) Once a string σ has been written down, you may also write down one or both of the strings σ0 or σ1. (Shortening Rule) For any string σ, once you have written down both σ0 and σ1 then you may write down σ.
The cut polytope of a graph arises in many fields. Although much is known about facets of the cut polytope of the complete graph, very little is known for general graphs. The study of Bell inequalities in quantum information science requires knowledge of the facets of the cut polytope of the complete bipartite graph or, more generally, the complete k-partite graph. Lifting is a central tool to prove certain inequalities are facet inducing for the cut polytope. In this paper we introduce a lifting operation, named triangular elimination, applicable to the cut polytope of a wide range of graphs. Triangular elimination is a specific combination of zero-lifting and Fourier-Motzkin elimination using the triangle inequality. We prove sufficient conditions for the triangular elimination of facet inducing inequalities to be facet inducing. The proof is based on a variation of the lifting lemma adapted to general graphs. The result can be used to derive facet inducing inequalities of the cut polytope of various graphs from those of the complete graph. We also investigate the symmetry of facet inducing inequalities of the cut polytope of the complete bipartite graph derived by triangular elimination.
The existing protocols that are used to prove that a committed number x lies in a specific interval mostly prove that the integer x is no less than a and then repeat the same method to prove that b is no less than x.In order to delete the repetition in these methods a new protocol is proposed by integrating the protocol that two committed numbers are equal with the protocol of the CFT proof.A verifier can be convinced that the committed number x is neither less than the integer a nor more than the integer b after the protocol is operated only once,and hence the exact proof that x lies in the interval is achieved.The proposed protocol is a statistical zero-knowledge proof.In contrast to Boudot's protocol,our method reduces an exponentiation operation;the communication quantity decreases from(16 176) bits to(13 222) bits,and the communication efficiency increases by 18.26 percent.
Smart play-out is a powerful technique for executing live sequence charts (LSCs). It uses verification techniques to help run a program, rather than to prove properties thereof. We extend smart play-out to cover a larger set of the LSC language features and to deal more efficiently with larger models. The extensions cover two key features of the rich version of LSCs, namely, time and forbidden elements. The former is crucial for systems with time constraints and/or time-driven behavior, and the latter allows specifying invariants and contracts on behavior. Forbidden elements can also help reduce the state space considered, thus enabling smart play-out to handle larger models.
It is proved that, when both randomization and interaction are allowed, the proofs that can be verified in polynomial time are exactly those proofs that can be generated with polynomial space. The interactive proofs introduced use only public coins, are accepted with probability one when the prover is honest, require only logarithmic workspace when the verifier is given a two-way access to his or her random tape, and by the use of known techniques can be turned into zero-knowledge proofs under the sole assumption that one-way functions exist.>
This paper proposes a new proof-based approach to safe evolution of distributed software systems. Specifically it extends the simple certification mechanism of proof-carrying code (PCC) to make it interactive and probabilistic, thereby devising code with interactive proof (CIP). With CIP, a code consumer is convinced, with overwhelming probability, of the existence and validity of a safety proof of a transmitted code through interaction with a code producer. The class of safety properties that are provable by CIP is larger than the class provable by PCC, provided that each code consumer is allowed to spend a reasonable amount of time on verification. Moreover, CIP can be further extended to devise code with zero-knowledge interactive proof (CZKIP). This concept is useful, for example, when the code producer wants to use the safety proof as a kind of "copyright" of the code.
The study of probabilistically verifiable proofs originated in the mid 1980s with the introduction of Interactive Proof Systems (IPs). The primary focus of research in this area in the '80s has been twofold: the role of zero-knowledge interactive proofs within cryptographic protocols, and characterizing which languages are efficiently interactively provable. In the 1990s, the focus of research on the topic shifted. Extensions of the interactive proof model, such as Multiprover Interactive Proofs (MIPs) and Probabilistically Checkable Proofs (PCPs), were considered with the intention of expanding our notion of what should be considered efficiently verifiable. In addition, researchers have taken a closer look at the exact resources (and tradeoffs amongst them) needed to verify a proof using various proof systems. This culminated in the important discovery that it is possible to verify NP statements (with a constant error probability) by only examining a constant number of bits of a PCP and using logarithmic amount of randomness. Perhaps, however, the most dramatic development has been the connection which was found between probabilistically verifiable proofs and proving hardness of approximation for optimization problems. It has been shown that a large variety of optimization versions of NP-hard problems (e.g., the maximum size of a clique in a graph, the minimum number of colors necessary to color a graph, and the maximum number of clauses satisfiable in a CNF formula) are not only NP-hard to solve exactly but also NP-hard to approximate in a very strong sense. The tools to establish hardness of approximation came directly from results on MIPs and PCPs. Indeed, almost every improvement in the efficiency of these proof systems translates directly into showing larger factors within which these optimization problems are hard to approximate. In 1994--1995 two exciting workshops were held at the Weizmann Institute in Israel on the new developments in probabilistically verifiable proofs and their applications to approximation problems, cryptography, program checking, and complexity theory at large. Over 60 papers were presented in the workshop series, and we are proud to include three of them in this special section. "On the Power of Finite Automata with Both Nondeterministic and Probabilistic States" by Anne Condon, Lisa Hellerstein, Samuel Pottle, and Avi Wigderson, considers constant round interactive proof systems where the verifier is restricted to use constant space and public coins. An equivalent characterization is finite automata with both nondeterministic and random states (npfa's), which accept their languages with a small probability of error. The paper shows that npfa's restricted to run in polynomial expected time accept only the regular languages in the case of npfa with 1-way input head, and that if Lis a nonregular language, then either L or its complement is not accepted by any npfa with a 2-way input head. "A Parallel Repetition Theorem" by Ran Raz, addresses and resolves the Parallel Repetition Conjecture which has eluded researchers for some time. The broader topic is what happens to the error probability of proof systems when they are composed. It has been known for awhile that sequential composition of proof systems (both single and multiprover interactive proofs) reduces the error exponentially, but this increases the number of rounds. For interactive proof systems, parallel repetition is known to reduce the error exponentially, and the Parallel Repetition Conjecture asserts that the same holds in a one-round two-prover proof system. Raz proves a constructive bound on the probability of error which indeed reduces at an exponential rate. The constant in the exponent is logarithmic in the total number of possible answers of the two provers, which means one can achieve two-prover one-round MIPs for NP statements with arbitrarily small constant error probability. This, in turn, has played a crucial role in further developments in the area and in particular in those reported in the next paper. "Free Bits, PCPs, and Nonapproximability---Towards Tight Results" by Mihir Bellare, Oded Goldreich, and Madhu Sudan, continues the investigation of PCPs and nonapproximability with emphasis on trying to get closer to tight results. The work consists of three parts. The first part presents several PCP proof systems for NP, based on a new error-correcting code called the Long Code. The second part shows that the connection between PCPs and hardness of approximation is not accidental. In particular, it shows that the transformation of a PCP for NP into hardness results for MaxClique can be reversed. Finally, the third part initiates a systematic investigation of the properties of PCPs as a function of the various parameters: randomness, query complexity, free-bit complexity, amortized free-bit complexity, proof size, etc. Two more papers submitted for this special section were not ready at this time for publication. They will appear in future issues of the SIAM Journal on Computing.
In this note, we present new zero-knowledge interactive proofs and arguments for languages in NP. To show that x ε L, with an error probability of at most 2-k, our zero-knowledge proof system requires O(|x|c1)+O(lgc2|x|)k ideal bit commitments, where c1 and c2 depend only on L. This construction is the first in the ideal bit commitment model that achieves large values of k more efficiently than by running k independent iterations of the base interactive proof system. Under suitable complexity assumptions, we exhibit zero knowledge arguments that require O(lgc|x|kl bits of communication, where c depends only on L, and l is the security parameter for the prover. This is the first construction in which the total amount of communication can be less than that needed to transmit the NP witness. Our protocols are based on efficiently checkable proofs for NP[4].