Many applications rely on accumulators and authenticated dictionaries, from timestamping certificate transparency and memory checking to blockchains and privacy-preserving decentralized electronic money, while Merkle tree and its variants are efficient for arbitrary element membership proofs, non-membership proofs, i.e., universal accumulators, and key-based membership proofs may require trees up to 256 levels for 128 bits of security, assuming binary tree, which makes it inefficient in...

In verifiable outsourcing, an untrusted server runs an expensive computation and produces a succinct proof (called a SNARK) of the results. In many scenarios, the computation accesses a RAM that the server maintains a commitment to (persistent RAM) or that is initially zero (volatile RAM). But, SNARKs for such scenarios are limited by the high overheads associated with existing techniques for RAM checking. We develop new proofs about volatile, persistent, and sparse persistent RAM that...

We study the complexity of memory checkers with computational security and prove the first general tight lower bound. Memory checkers, first introduced over 30 years ago by Blum, Evans, Gemmel, Kannan, and Naor (FOCS '91, Algorithmica '94), allow a user to store and maintain a large memory on a remote and unreliable server by using small trusted local storage. The user can issue instructions to the server and after every instruction, obtain either the correct value or a failure (but not...

Homomorphic encryption (HE) enables computation on encrypted data, which in turn facilitates the outsourcing of computation on private data. However, HE offers no guarantee that the returned result was honestly computed by the cloud. In order to have such guarantee, it is necessary to add verifiable computation (VC) into the system. The most efficient recent works in VC over HE focus on verifying operations on the ciphertext space of the HE scheme, which usually lacks the algebraic...

When outsourcing a database to an untrusted remote server, one might want to verify the integrity of contents while accessing it. To solve this, Blum et al. [FOCS `91] propose the notion of memory checking. Memory checking allows a user to run a RAM program on a remote server, with the ability to verify integrity of the storage with small local storage. In this work, we define and initiate the formal study of memory checking for Parallel RAMs (PRAMs). The parallel RAM...

Zero-Knowledge Virtual Machines (ZKVMs) have gained traction in recent years due to their potential applications in a variety of areas, particularly blockchain ecosystems. Despite tremendous progress on ZKVMs in the industry, no formal definitions or security proofs have been established in the literature. Due to this lack of formalization, existing protocols exhibit significant discrepancies in terms of problem definitions and performance metrics, making it difficult to analyze and compare...

Motivated by the extended deployment of authenticated data structures (e.g., Merkle Patricia Tries) for verifying massive amounts of data in blockchain systems, we begin a systematic study of the I/O efficiency of such systems. We first explore the fundamental limitations of memory checking, a previously-proposed abstraction for verifiable storage, in terms of its locality---a complexity measure that we introduce for the first time and is defined as the number of non-contiguous memory...

Persistent fault analysis is a novel and efficient cryptanalysis method. The persistent fault attacks take advantage of a persistent fault injected in a non-volatile memory, then present on the device until the reboot of the device. Contrary to classical physical fault injection, where differential analysis can be performed, persistent fault analysis requires new analyses and dedicated countermeasures. Persistent fault analysis requires a persistent fault injected in the S-box such that the...

The problem of decoding random codes is a fundamental problem for code-based cryptography, including recent code-based candidates in the NIST post-quantum standardization process. In this paper, we present a novel sieving-style information-set decoding (ISD) algorithm, addressing the task of solving the syndrome decoding problem. Our approach involves maintaining a list of weight-$2p$ solution vectors to a partial syndrome decoding problem and then creating new vectors by identifying pairs...

Oblivious RAM (ORAM), introduced by Goldreich and Ostrovsky (J. ACM `96), is a primitive that allows a client to perform RAM computations on an external database without revealing any information through the access pattern. For a database of size $N$, well-known lower bounds show that a multiplicative overhead of $\Omega(\log N)$ in the number of RAM queries is necessary assuming $O(1)$ client storage. A long sequence of works culminated in the asymptotically optimal construction of Asharov,...

The Noise protocol framework defines a succinct notation and execution framework for a large class of 59 secure channel protocols, some of which are used in popular applications such as WhatsApp and WireGuard. We present a verified implementation of a Noise protocol compiler that takes any Noise protocol, and produces an optimized C implementation with extensive correctness and security guarantees. To this end, we formalize the complete Noise stack in F*, from the low-level cryptographic...

Timing attacks are among the most devastating side-channel attacks, allowing remote attackers to retrieve secret material, including cryptographic keys, with relative ease. In principle, “these attacks are not that hard to mitigate”: the basic intuition, captured by the constant-time criterion, is that control-flow and memory accesses should be independent from secrets. Furthermore, there is a broad range of tools for automatically checking adherence to this intuition. Yet, these attacks...

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed...

We initiate the study of verifiable capacity-bound function (VCBF). The main VCBF property imposes a strict lower bound on the number of bits read from memory during evaluation (referred to as minimum capacity). No adversary, even with unbounded computational resources, should produce an output without spending this minimum memory capacity. Moreover, a VCBF allows for an efficient public verification process: Given a proof-of-correctness, checking the validity of the output takes...

Fast Near collision attacks on the stream ciphers Grain v1 and A5/1 were presented at Eurocrypt 2018 and Asiacrypt 2019 respectively. They use the fact that the entire internal state can be split into two parts so that the second part can be recovered from the first one which can be found using the keystream prefix and some guesses of the key materials. In this paper we reevaluate the complexity of these attacks and show that actually they are inferior to previously known results. Basically,...

High-assurance cryptography leverages methods from program verification and cryptography engineering to deliver efficient cryptographic software with machine-checked proofs of memory safety, functional correctness, provable security, and absence of timing leaks. Traditionally, these guarantees are established under a sequential execution semantics. However, this semantics is not aligned with the behavior of modern processors that make use of speculative execution to improve performance....

Routing protocol for Low power and lossy network (RPL) is a standardized optimal protocol for routing in Internet of Things (IoT). The constrained wireless sensor network in IoT is characterized by lack of processing speed, low power and low memory. Sometimes various network attacks enabling the RPL network affect the network performance dismally. This leads to drastic variation in energy consumption at nodes and disturb the RPL network protocol structure. This leads to reduced processing...

Achieving fairness and soundness in non-simultaneous rational secret sharing schemes has proved to be challenging. On the one hand, soundness can be ensured by providing side information related to the secret as a check, but on the other, this can be used by deviant players to compromise fairness. To overcome this, the idea of incorporating a time delay was suggested in the literature: in particular, time-delay encryption based on memory-bound functions has been put forth as a solution. In...

In this paper, we revisit the difference enumeration technique for LowMC and develop new algebraic techniques to achieve efficient key-recovery attacks. In the original difference enumeration attack framework, an inevitable step is to precompute and store a set of intermediate state differences for efficient checking via the binary search. Our first observation is that Bar-On et al.'s general algebraic technique developed for SPNs with partial nonlinear layers can be utilized to fulfill the...

An important primitive in ensuring security of modern systems-on-chip designs are protocols for authenticated firmware load. These loaders read a firmware binary image from an untrusted input device, authenticate the image using cryptography and load the image into memory for execution if authentication succeeds. While these protocols are an essential part of the hardware root of trust in almost all modern computing devices, verification techniques for reasoning about end-to-end security of...

Dilithium is a round 2 candidate for digital signature schemes in NIST initiative for post-quantum cryptographic schemes. Since Dilithium is built upon the “Fiat Shamir with Aborts” framework, its signing procedure performs rejection sampling of its signatures to ensure they do not leak information about the secret key. Thus, the signing procedure is iterative in nature with a number of rejected iterations, which serve as unnecessary overheads hampering its overall performance. As a first...

Code update is a very useful tool commonly used in low-end embedded devices to improve the existing functionalities or patch discovered bugs or vulnerabilities. If the update protocol itself is not secure, it will only bring new threats to embedded systems. Thus, a secure code update mechanism is required. However, existing solutions either rely on strong security assumptions, or result in considerable storage and computation consumption, which are not practical for resource-constrained...

Keeping correct and informative log files is crucial for system maintenance, security and forensics. Cryptographic logging schemes offer integrity checks that protect a log file even in the case where an attacker has broken into the system. A relatively recent feature of these schemes is resistance against truncations, i.e. the deletion and/or replacement of the end of the log file. This is especially relevant as system intruders are typically interested in manipulating the later log...

We present an algorithm for the approximate $k$-List problem for the Euclidean distance that improves upon the Bai-Laarhoven-Stehle (BLS) algorithm from ANTS'16. The improvement stems from the observation that almost all the solutions to the approximate $k$-List problem form a particular configuration in $n$-dimensional space. Due to special properties of configurations, it is much easier to verify whether a $k$-tuple forms a configuration rather than checking whether it gives a solution to...

We show how short cycles in the state space of a cryptographic algorithm can be used to mount a fault attack on its implementation which results in a full secret key recovery. The attack is based on the assumption that an attacker can inject a transient fault at a precise location and time of his/her choice and more than once. We present an algorithm which uses a SAT-based bounded model checking for finding all short cycles of a given length. The existing Boolean Decision Diagram (BDD) based...

In this paper we study a parity check based countermeasure proposed by Chen et al. that thwarts their attack by detecting byte fault injection during the AES key schedule process. We provide a generalization of their approach that allows to derive parity equations for every AES sizes not given by the authors. We analyze why Chen et al. countermeasure does not properly works. Doing so we are able to extend the coverage of the fault detection to the full expanded key. Finally we suggest...

The challenges faced in securing embedded computing systems against multifaceted memory safety vulnerabilities have prompted great interest in the development of memory safety countermeasures. These countermeasures either provide protection only against their corresponding type of vulnerabilities, or incur substantial architectural modifications and overheads in order to provide complete safety, which makes them infeasible for embedded systems. In this paper, we propose M-MAP: a...

Extensive use of third party IP cores (e.g., HDL, netlist) and open source tools in the FPGA application design and development process in conjunction with the inadequate bitstream protection measures have raised crucial security concerns in the past for reconfigurable hardware systems. Designing high fidelity and secure methodologies for FPGAs are still infancy and in particular, there are almost no concrete methods/techniques that can ensure trust in FPGA applications not entirely designed...

Cache-based attacks are a class of side-channel attacks that are particularly effective in virtualized or cloud-based environments, where they have been used to recover secret keys from cryptographic implementations. One common approach to thwart cache-based attacks is to use \emph{constant-time} implementations, i.e.\, which do not branch on secrets and do not perform memory accesses that depend on secrets. However, there is no rigorous proof that constant-time implementations are...

In this paper, we introduce a new approach to side-channel key recovery, that combines the low time/memory complexity and noise tolerance of standard (divide and conquer) differential power analysis with the optimal data complexity of algebraic side-channel attacks. Our fundamental contribution for this purpose is to change the way of expressing the problem, from the system of equations used in algebraic attacks to a code, essentially inspired by low density parity check codes. We then show...

Proofs of computational effort were devised to control denial of service attacks. Dwork and Naor (CRYPTO ’92), for example, proposed to use such proofs to discourage spam. The idea is to couple each email message with a proof of work that demonstrates the sender performed some computational task. A proof of work can be either CPU-bound or memory-bound. In a CPU-bound proof, the prover must compute a CPU-intensive function that is easy to check by the verifier. A memory-bound proof, instead,...

We describe a method for efficiently hashing multiple messages of different lengths. Such computations occur in various scenarios, and one of them is when an operating system checks the integrity of its components during boot time. These tasks can gain performance by parallelizing the computations and using SIMD architectures. For such scenarios, we compare the performance of a new 4-buffers SHA-256 S-HASH implementation, to that of the standard serial hashing. Our results are measured on...

Memory checking studies the problem of cryptographically verifying the correctness of untrusted indexed storage. After a series of results yielding checkers with $O(\log n)$ query complexity, Dwork, Naor, Ruthblum and Vaikuntanathan~\cite{naor-lower-mm08} derived an $\Omega(\log n/\log \log n)$ lower bound on the query complexity of any checker operating on memory words of polylogarithmic size, where $n$ is the number of memory indices. In view of this lower bound, we make the following two...

We study the problem of authenticating a \emph{dynamic table} with $n$ entries in the authenticated data structures model, which is related to memory checking. We present the first dynamic authenticated table that is \emph{update-optimal}, using a \emph{lattice-based} construction. In particular, the update time is $O(1)$, improving in this way the ``a priori'' $O(\log n)$ update bounds for previous constructions, such as the Merkle tree. Moreover, the space used by our data structure is...

In this paper, we define and explore the notion of a _proof of retrievability_ (POR). A POR enables an archive or back-up service (prover) to demonstrate to a user (verifier) that it has ``possession'' of a file F, that is, that the archive retains data sufficient for the user to retrieve F in its entirety. A POR may be viewed as a kind of cryptographic proof of knowledge (POK), but one specially designed to handle a _large_ file (or bitstring) F. We explore POR protocols here in which the...

Suppose you want to store a large file on a remote and unreliable server. You would like to verify that your file has not been corrupted, so you store a small private (randomized)``fingerprint'' of the file on your own computer. This is the setting for the well-studied authentication problem, and the size of the required private fingerprint is well understood. We study the problem of sub-linear authentication: suppose you would like to encode and store your file in a way that allows you to...

In Year 2005, Internet users were twice more likely to receive unsolicited electronic messages, known as spams, than regular emails. Proof of work protocols are designed to deter such phenomena and other denial-of-service attacks by requiring computed stamps based on hard-to-solve problems with easy-to-verify solutions. As cpu-intensive computations are badly hit over time by Moore's law, memory-bound computations have been suggested to deal with heterogeneous hardware. We introduce new...

While bringing considerable flexibility and extending the horizons of mobile computing, mobile code raises major security issues. Hence, mobile code, such as Java applets, needs to be analyzed before execution. The byte-code verifier checks low-level security properties that ensure that the downloaded code cannot bypass the virtual machine's security mechanisms. One of the statically ensured properties is {\sl type safety}. The type-inference phase is the overwhelming resource-consuming part...