Ethereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Virtual Machine (EVM). EVM executes bytecode on simple stack machine. Programmers do not usually write code; instead, they can program in JavaScript-like language, Solidity, that compiles bytecode. Since main purpose of execute smart contracts manage and transfer digital assets (called Ether), security paramount importance. However, writing secure be...

We present CrypTFlow, a first of its kind system that converts TensorFlow inference code into Secure Multi-party Computation (MPC) protocols at the push button. To do this, we build three components. Our component, Athos, is an end-to-end compiler from to variety semihonest MPC protocols. The second Porthos, improved semi-honest 3-party protocol provides significant speedups for like applications. Finally, provide malicious secure protocols, our third Aramis, novel technique uses hardware...

In a Secure Multiparty Computation (SMC), mutually distrusting parties use cryptographic techniques to cooperatively compute over their private data, in the process each party learns only explicitly revealed outputs. this paper, we present Wysteria, high-level programming language for writing SMCs. As with past languages, like Fairplay, Wysteria compiles secure computations circuits that are executed by an underlying engine. Unlike work, provides support mixed-mode programs, which combine...

We present Low*, a language for low-level programming and verification, its application to high-assurance optimized cryptographic libraries. Low* is shallow embedding of small, sequential, well-behaved subset C in F*, dependently- typed variant ML aimed at program verification. Departing from ML, does not involve any garbage collection or implicit heap allocation; instead, it has structured memory model à la CompCert, provides the control required writing efficient security-critical code. By...

We present EzPC, a secure two-party computation (2PC) framework that generates efficient 2PC protocols from high-level, easy-to-write programs. EzPC provides formal correctness and security guarantees while maintaining performance scalability. Previous language frameworks, such as CBMC-GC, ObliVM, SMCL, Wysteria, generate use either arithmetic or boolean circuits exclusively. Our compiler is the first to combine both for better performance. empirically demonstrate of generated by comparable...

JavaScript's flexible semantics makes writing correct code hard and secure extremely difficult. To address the former problem, various forms of gradual typing have been proposed, such as Closure TypeScript. However, supporting all common programming idioms is not easy; for example, TypeScript deliberately gives up type soundness convenience. In this paper, we propose a system implementation techniques that provide important safety security guarantees.

Data replication is crucial for enabling fault tolerance and uniform low latency in modern decentralized applications. Replicated Types (RDTs) have emerged as a principled approach developing replicated implementations of basic data structures such counter, flag, set, map, etc. While the correctness RDTs generally specified using notion strong eventual consistency--which guarantees that replicas received same set updates would converge to state--a more expressive specification which relates...

Gradual typing lets programmers evolve their dynamically typed programs by gradually adding explicit type annotations, which confer benefits like improved performance and fewer run-time failures. However, we argue that such evolution often requires a giant leap, inference can offer crucial missing step. If omitted annotations are interpreted as unknown types, rather than the dynamic type, then static types be inferred, thereby removing unnecessary assumptions of type. The remaining may...

Dijkstra monads enable a dependent type theory to be enhanced with support for specifying and verifying effectful code via weakest preconditions. Together their closely related counterparts, Hoare monads, they provide the basis on which verification tools like F*, Type Theory (HTT), Ynot are built. We show that can derived "for free" by applying continuation-passing style (CPS) translation standard monadic definitions of underlying computational effects. Automatically deriving in this way...

We present CrypTFlow2, a cryptographic framework for secure inference over realistic Deep Neural Networks (DNNs) using 2-party computation. CrypTFlow2 protocols are both correct -- i.e., their outputs bitwise equivalent to the cleartext execution and efficient they outperform state-of-the-art in latency scale. At core of we have new 2PC comparison division, designed carefully balance round communication complexity tasks. Using first ImageNet-scale DNNs like ResNet50 DenseNet121. These at...

High-performance cryptographic libraries often mix code written in a high-level language with assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding subset x64 assembly F* that allows efficient verification both its interoperation C generated from F*. The key idea is to use computational power dependent type system's checker run verified verification-condition generator during checking. This customize condition sent by...

Loop invariants are fundamental to reasoning about programs with loops. They establish properties a given loop's behavior. When they additionally inductive, become useful for the task of formal verification that seeks strong mathematical guarantees program's runtime The inductiveness ensures can be checked locally without consulting entire program, thus indispensable artifacts in proof correctness. Finding inductive loop is an undecidable problem, and despite long history research towards...

Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful theories can provide a foundation which build semantics for more complex programming constructs and program logics, extending the reasoning principles apply host theory itself. Concretely, our main contribution is concurrent separation logic (CSL) F ⋆ proof assistant in manner enables dependently typed, programs make use of concurrency be specified verified using...

Relational properties describe multiple runs of one or more programs. They characterize many useful notions security, program refinement, and equivalence for programs with diverse computational effects, they have received much attention in the recent literature. Rather than developing separate tools special classes effects relational properties, we advocate using a general purpose proof assistant as unifying framework verification effectful The essence our approach is to model computations...

With an eye toward performance, interoperability, or legacy concerns, low-level system software often must parse binary encoded data formats. Few tools are available for this task, especially since the formats involve a mixture of arithmetic and dependence, beyond what can be handled by typical parser generators. As such, parsers written hand in languages like C, with inevitable errors leading to security vulnerabilities.

We present a compiler-based scheme to protect the confidentiality of sensitive data in low-level applications (e.g. those written C) presence an active adversary. In our scheme, programmer marks by lightweight annotations on top-level definitions source code. The compiler then uses combination static dataflow analysis, runtime instrumentation, and novel taint-aware form control-flow integrity prevent leaks even attacks. To reduce overheads, memory layout.

Steel is a language for developing and proving concurrent programs embedded in F ⋆ , dependently typed programming proof assistant. Based on SteelCore, separation logic (CSL) formalized our work focuses exposing the rules of form that enables proofs to be effectively co-developed. Our main contributions include new formulation Hoare quintuples involving both first-order logic, enabling efficient verification condition (VC) generation discharge using combination tactics SMT solving. We relate...

We present FastVer, a high-performance key-value store with strong data integrity guarantees. FastVer is built as an extension of FASTER, open-source, store. It offers the same API FASTER plus additional verify() method that detects if unauthorized attacker tampered database and checks whether results all read operations are consistent historical updates. based on novel approach combines advantages Merkle trees deferred memory verification. show this achieves one to two orders magnitudes...

We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that property witnessed in prior can be soundly recalled current state, provided (1) according given preorder, and (2) preserved by this preorder. In many scenarios, such monotonic reasoning yields concise modular proofs, saving need for explicit program invariants. distill our approach into monotonic-state monad , general yet compact interface Hoare-style about dependently typed...

Current proposals for adding gradual typing to JavaScript, such as Closure, TypeScript and Dart, forgo soundness deal with issues of scale, code reuse, popular programming patterns. We show how address these in practice while retaining soundness. design implement a new type system, prototyped expediency 'Safe' compilation mode TypeScript. Our compiler achieves by enforcing stricter static checks embedding residual runtime compiled code. It emits plain JavaScript that runs on stock virtual...

The Rust programming language, with its safety guarantees, has established itself as a viable choice for low-level systems language over the traditional, unsafe alternatives like C/C++. These guarantees come from strong ownership-based type system, well primitive support features closures, pattern matching, etc., that make code more concise and amenable to reasoning. unique also pose steep learning curve programmers. This paper presents tool called RustAssistant leverages emergent...

JavaScript's flexible semantics makes writing correct code hard and secure extremely difficult. To address the former problem, various forms of gradual typing have been proposed, such as Closure TypeScript. However, supporting all common programming idioms is not easy; for example, TypeScript deliberately gives up type soundness convenience. In this paper, we propose a system implementation techniques that provide important safety security guarantees. We present TS# , source-to-source...