We propose hinTS — a new threshold signature scheme built on top of the widely used BLS signatures. Our scheme enjoys the following attractive features:A silent setup process where the joint public key of the parties is computed as a deterministic function of their locally computed public keys.Support for dynamic choice of thresholds and signers, after the silent setup, without further interaction.Support for general access policies; in particular, native support for weighted thresholds with zero additional overhead over standard threshold setting.Strong security guarantees, including proactive security and forward security.We prove the security of hinTS in the algebraic group model, and also provide an open-source implementation. Our scheme outperforms all prior proposals that avoid distributed key generation in terms of aggregation time, signature size, and verification time (as well as other qualitative measures). As an example, the aggregation time in hinTS for 1000 signers is under 0.5 seconds, while both signing and verification are constant time algorithms, taking 1 ms and 17.5 ms, respectively.The key technical contribution of our work involves the design of special-purpose succinct proofs to efficiently prove the well-formedness of aggregated public keys. Our solution uses public "hints" released by the signers as part of their public keys (hence the name hinTS).

We propose SublonK --- a new succinct non-interactive argument of knowledge (SNARK). SublonK is the first SNARK that achieves both a constant proof size and prover runtime that grows only with the size of the ``active part'' of the executed circuit (i.e., *sub-linear* in the size of the entire circuit) while being *black-box in cryptography*. For instance, consider circuits encoding conditional execution, where only a fraction of the circuit is exercised by the input. For such circuits, the prover runtime in SublonK grows only with the exercised execution path. Our new construction builds on PlonK [Gabizon-Williamson-Ciobotaru, EPRINT'19], a popular state-of-the-art practical zkSNARK, and preserves all its great features --- constant size proofs, constant time proof verification, a circuit-independent universal setup, and support for custom gates and lookup gates. Our techniques are useful for a wide range of applications that involve a circuit executing k steps, where at each step, a (possibly different) s-sized segment is executed from a choice of n segments. Our prover cost for such circuits is O(ks(log (ks) + log(n))). Finally, we show that our improvements are not purely asymptotic. Specifically, we demonstrate the concrete efficiency of SublonK using zkRollups as an example application. Based on our implementation, for parameter choices derived from rollup contracts on Ethereum, n =8, k = 128, s= 2^{16}, the SublonK prover is approximately 4.8x faster than the PlonK prover, and proofs in SublonK are 2.4KB and can be verified in under 50ms.

We introduce a new notion of multiverse threshold signatures (MTS). In an MTS scheme, multiple universes – each defined by a set of (possibly overlapping) signers, their weights, and a specific security threshold – can co-exist. A universe can be (adaptively) created via a non-interactive asynchronous setup. Crucially, each party in the multiverse holds constant-sized keys and releases compact signatures with size and computation time both independent of the number of universes. Given sufficient partial signatures over a message from the members of a specific universe, an aggregator can produce a short aggregate signature relative to that universe.We construct an MTS scheme building on BLS signatures. Our scheme is practical, and can be used to reduce bandwidth complexity and computational costs in decentralized oracle networks. As an example data point, consider a multiverse containing 2000 nodes and 100 universes (parameters inspired by Chainlink’s use in the wild), each of which contains arbitrarily large subsets of nodes and arbitrary thresholds. Each node computes and outputs 1 group element as its partial signature; the aggregator performs under 0.7 seconds of work for each aggregate signature, and the final signature of size 192 bytes takes 6.4 ms (or 198K EVM gas units) to verify. For this setting, prior approaches, when used to construct MTS, yield schemes that have one of the following drawbacks: (i) partial signatures that are 48× larger, (ii) have aggregation times 311× worse, or (iii) have signature size 39× and verification gas costs 3.38× larger. We also provide an open-source implementation and a detailed evaluation.

Timed-release encryption can encrypt a message to a future time such that it can only be decrypted after that time. Potential applications include sealed bid auctions, scheduled confidential transactions, and digital time capsules. To enable such applications as decentralized smart contracts, we explore how to use timed-release encryption on blockchains.

Threshold cryptography enables cryptographic operations while keeping the secret keys distributed at all times. Agrawal et al. (CCS'18) propose a framework for Distributed Symmetric-key Encryption (DiSE). They introduce a new notion of Threshold Symmetric-key Encryption (TSE), in that encryption and decryption are performed by interacting with a threshold number of servers. However, the necessity for interaction on each invocation limits performance when encrypting large datasets, incurring heavy computation and communication on the servers.

Many important cryptographic primitives offer probabilistic guarantees of security that can be specified as quantitative hyperproperties; these are specifications that stipulate the existence of a certain number of traces in the system satisfying certain constraints. Verification of such hyperproperties is extremely challenging because they involve simultaneous reasoning about an unbounded number of different traces. In this paper, we introduce a technique for verifying quantitative hyperproperties based on the notion of trace enumeration relations. These relations allow us to reduce the problem of trace-counting into one of model-counting of formulas in first-order logic. We also introduce a set of inference rules for machine-checked reasoning about the number of satisfying solutions to first-order formulas (aka model counting). Putting these two components together enables semi-automated verification of quantitative hyperproperties on infinite-state systems. We use our methodology to prove confidentiality of access patterns in Path ORAMs of unbounded size, soundness of a simple interactive zero-knowledge proof protocol as well as other applications of quantitative hyperproperties studied in past work.

Recent proposals for trusted hardware platforms, such as Intel SGX and the MIT Sanctum processor, offer compelling security features but lack formal guarantees. We introduce a verification methodology based on a trusted abstract platform (TAP), a formalization of idealized enclave platforms along with a parameterized adversary. We also formalize the notion of secure remote execution and present machine-checked proofs showing that the TAP satisfies the three key security properties that entail secure remote execution: integrity, confidentiality and secure measurement. We then present machine-checked proofs showing that SGX and Sanctum are refinements of the TAP under certain parameterizations of the adversary, demonstrating that these systems implement secure enclaves for the stated adversary models.

Trusted hardware primitives such as Intel's SGX instructions provide applications with a protected address space, called an enclave, for trusted code and data. However, building enclaves that preserve confidentiality of sensitive data continues to be a challenge. The developer must not only avoid leaking secrets via the enclave's outputs but also prevent leaks via side channels induced by interactions with the untrusted platform. Recent attacks have demonstrated that simply observing the page faults incurred during an enclave's execution can reveal its secrets if the enclave makes data accesses or control flow decisions based on secret values. To address this problem, a developer needs compilers to automatically produce confidential programs, and verification tools to certify the absence of secret-dependent page access patterns (a property that we formalize as page-access obliviousness). To that end, we implement an efficient compiler for a type and memory-safe language, a compiler pass that enforces page-access obliviousness with low runtime overheads, and an automatic, modular verifier that certifies page-access obliviousness at the machine-code level, thus removing the compiler from our trusted computing base. We evaluate this toolchain on several machine learning algorithms and image processing routines that we run within SGX enclaves.

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running in a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challenging. We present a methodology for designing such applications in a way that enables certifying their confidentiality. Our methodology consists of forcing the application to communicate with the external world through a narrow interface, compiling it with runtime checks that aid verification, and linking it with a small runtime that implements the narrow interface. The runtime includes services such as secure communication channels and memory management. We formalize this restriction on the application as Information Release Confinement (IRC), and we show that it allows us to decompose the task of proving confidentiality into (a) one-time, human-assisted functional verification of the runtime to ensure that it does not leak secrets, (b) automatic verification of the application's machine code to ensure that it satisfies IRC and does not directly read or corrupt the runtime's internal state. We present /CONFIDENTIAL: a verifier for IRC that is modular, automatic, and keeps our compiler out of the trusted computing base. Our evaluation suggests that the methodology scales to real-world applications.

Security-critical applications constantly face threats from exploits in lower computing layers such as the operating system, virtual machine monitors, or even attacks from malicious administrators. To help protect application secrets from such attacks, there is increasing interest in hardware implementations of primitives for trusted computing, such as Intel's Software Guard Extensions (SGX) instructions. These primitives enable hardware protection of memory regions containing code and data, and provide a root of trust for measurement, remote attestation, and cryptographic sealing. However, vulnerabilities in the application itself, such as the incorrect use of SGX instructions or memory safety errors, can be exploited to divulge secrets. In this paper, we introduce a new approach to formally model these primitives and formally verify properties of so-called enclave programs that use them. More specifically, we create formal models of relevant aspects of SGX, develop several adversary models, and present a sound verification methodology (based on automated theorem proving and information flow analysis) for proving that an enclave program running on SGX does not contain a vulnerability that causes it to reveal secrets to the adversary. We introduce Moat, a tool which formally verifies confidentiality properties of applications running on SGX. We evaluate Moat on several applications, including a one time password scheme, off-the-record messaging, notary service, and secure query processing.

This work presents a methodology that parallelizes the simulation of mixed-abstraction level SystemC models across multicore CPUs, and graphics processing units (GPUs) for improved simulation performance. Given a SystemC model, we partition it into processes suitable for GPU execution and CPU execution. We convert the processes identified for GPU execution into GPU kernels with additional SystemC wrapper processes that invoke these kernels. The wrappers enable seamless communication of events in all directions between the GPUs and CPUs. We alter the OSCI SystemC simulation kernel to allow parallel execution of processes. Hence, we co-simulate in parallel, the SystemC processes on multiple CPUs, and the GPU kernels on the GPUs; exploit both the CPUs, and GPUs for faster simulation. We experiment with synthetic benchmarks and a set-top box case study.

This paper presents a high-level synthesis framework called synASM that synthesizes abstract state machines (ASMs) to VHDL for field-programmable gate arrays (FPGAs). In particular, this paper focuses on the specification, scheduling, and synthesis of parallel and timed constructs. ASMs possess well-defined formal semantics for sequential and parallel computation, and their composition. We extend ASMs to support the specification of timing requirements, which we call timed constructs. We also describe the composition of timed constructs with sequential and parallel computation. A key contribution of this paper is the extension of the force-directed scheduling algorithm to support both parallel and timed constructs. We implement the synthesis back-end in synASM that targets FPGAs. Our experiments show improvements of up to 52% in lookup table usage and 34% in total area for certain examples.

This work presents a high-level synthesis methodology that uses the abstract state machines (ASMs) formalism as an intermediate representation (IR). We perform scheduling and allocation on this IR, and generate synthesizable VHDL. We have the following advantages when using ASMs as an IR: 1) it allows the specification of both sequential and parallel computation, 2) it supports an extension of a clean timing model based on an interpretation of the sequential semantics, and 3) it has well-defined formal semantics, which allows the integration of formal methods into the methodology. While we specify our designs using ASMs, we do not mandate this. Instead, one can create translators that convert the algorithmic specifications from C-like languages into their equivalent ASM specifications. This makes the hardware synthesis transparent to the designer. We experiment our methodology with examples of a FIR, microprocessor, and an edge detector. We synthesize these designs and validate our designs on an FPGA.

This work extends force-directed scheduling (FDS) to support specification constructs that express parallelism and timing behaviours. We select the FDS algorithm because it maximizes the amount of resource sharing, and it naturally supports constructs for parallelism. However, timed constructs are not supported. As a result, we propose timed FDS (TFDS) that optimizes over parallel, timed and untimed constructs. In doing so, we make the following four contributions: 1) we extend the definition of control data flow graphs (CDFGs) to define timed CDFGs (TCDFGs), 2) we define a scheduling algorithm for timed constructs called TIME, 3) we extend the definition of mobility used in FDS, and 4) we present optimizations for a composition of parallel, timed and untimed constructs to better aid FDS. We implement our extensions in a high-level synthesis framework based on the abstract state machine formalism, and we generate synthesizable VHDL. We experiment with several examples such as FIR, edge detector, and a differential equation solver, and target them onto an Altera DE2 FPGA. Some of these experiments show improvements of up to 52% in circuit area when compared to their unoptimized counterparts.