Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm—and attackers can exploit buffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. Memory- Safe WebAssembly (MSWasm) proposes to extend Wasm with language-level memory-safety abstractions to precisely address this problem. In this paper, we build on the original MSWasm position paper to realize this vision. We give a precise and formal semantics of MSWasm, and prove that well-typed MSWasm programs are, by construction, robustly memory safe. To this end, we develop a novel, language-independent memory-safety property based on colored memory locations and pointers. This property also lets us reason about the security guarantees of a formal C-to-MSWasm compiler—and prove that it always produces memory-safe programs (and preserves the semantics of safe programs). We use these formal results to then guide several implementations: Two compilers of MSWasm to native code, and a C-to-MSWasm compiler (that extends Clang). Our MSWasm compilers support different enforcement mechanisms, allowing developers to make security-performance trade-offs according to their needs. Our evaluation shows that on the PolyBenchC suite, the overhead of enforcing memory safety in software ranges from 22% (enforcing spatial safety alone) to 198% (enforcing full memory safety), and 51.7% when using hardware memory capabilities for spatial safety and pointer integrity. More importantly, MSWasm’s design makes it easy to swap between enforcement mechanisms; as fast (especially hardware-based) enforcement techniques become available, MSWasm will be able to take advantage of these advances almost for free.
more »
« less
Viaduct: an extensible, optimizing compiler for secure distributed programs
Modern distributed systems involve interactions between principals with limited trust, so cryptographic mechanisms are needed to protect confidentiality and integrity. At the same time, most developers lack the training to securely employ cryptography. We present Viaduct, a compiler that transforms high-level programs into secure, efficient distributed realizations. Viaduct's source language allows developers to declaratively specify security policies by annotating their programs with information flow labels. The compiler uses these labels to synthesize distributed programs that use cryptography efficiently while still defending the source-level security policy. The approach is general, and can be easily extended with new security mechanisms. Our implementation of the compiler comes with an extensible runtime system that includes plug-in support for multiparty computation, commitments, and zero-knowledge proofs. We have evaluated the system on a set of benchmarks, and the results indicate that our approach is feasible and can use cryptography in efficient, nontrivial ways.
more »
« less
- Award ID(s):
- 1704788
- NSF-PAR ID:
- 10328578
- Date Published:
- Journal Name:
- PLDI 2021
- Page Range / eLocation ID:
- 740 to 755
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We propose a method for optimizing the energy efficiency of software code running on small computing devices in the Internet of Things (IoT) that are powered exclusively by electricity harvested from ambient energy in the environment. Due to the weak and unstable nature of the energy source, it is challenging for developers to manually optimize the software code to deal with mismatch between the intermittent power supply and the computation demand. Our method overcomes the challenge by using a combination of three techniques. First, we use static program analysis to automatically identify opportunities for precomputation, i.e., computation that may be performed ahead of time as opposed to just in time. Second, we optimize the precomputation policy, i.e., a way to split and reorder steps of a computation task in the original software to match the intermittent power supply while satisfying a variety of system requirements; this is accomplished by formulating energy optimization as a constraint satisfiability problem and then solving the problem using an off-the-shelf SMT solver. Third, we use a state-of-the-art compiler platform (LLVM) to automate the program transformation to ensure that the optimized software code is correct by construction. We have evaluated our method on a large number of benchmark programs, which are C programs implementing secure communication protocols that are popular for energy-harvesting IoT devices. Our experimental results show that the method is efficient in optimizing all benchmark programs. Furthermore, the optimized programs significantly outperform the original programs in terms of energy efficiency and latency, and the overall improvement ranges from 2.3X to 36.7X.more » « less
-
Cybersecurity continues to be a critical aspect within every computing division, especially in the realm of operating system (OS) development. The OS resides at the lower layer above the hardware in the computing hierarchy. If the layers above the OS are well hardened, a security flaw in the OS will compromise the resources in those higher layers. Although several learning resources and courses are available for OS security, they are taught in advanced UG or graduate-level computer security classes. In this work, we develop cybersecurity educational modules that instructors can adoptin their OS courses to emphasize security in OS while teaching its concepts. The goal of this work is to engage students in learning security aspects in OS, while learning its concepts. It will give students a good understanding of different security concepts and how they are implemented in the OS. Towards this, we develop security educational modules for an OS course that will be available to the instructors for adoption in their courses. These modules are designed to be used in a UG-level OS course. To work on these modules, students should be familiar with C programming and OS concepts taught in the class. The modules are intended to be completed within the course of a semester. To achieve this goal, we organize them into three mini-projects witheach can be completed within a few weeks. We chose xv6 as the platform due to its popularity as an educational OS for developing the modules. To develop the modules, we referred to the recent version of a popular OS textbook for the security concepts. The topics discussed in it include authentication, authorization, cryptography, and distributed system security. We kept our educational modules mostly aligned with these topics except distributed system security. We also included a module for implementing a defense mechanism against buffer-overflow attacks, a famous software vulnerability. We created three mini-projects for these modules, each accompanied by proper documentation and a GitHub repository. Two versions are created for each project, one for a student’s assignment available in the repository and another as a solution version for instructors. The first project implements a user authentication system in xv6. Students will implement various specifications such as password structure with encryption and programs such as useradd, passwd, whoami, and login. The implementation guidelines are provided in the documentation, along with skeleton code. The authorization project implements the Unix-style access control system. In this project, students will modify and create various structures and functions within the xv6 kernel. The last project is to build a defense mechanism against buffer-overflow using Address Space Layout Randomization (ASLR). Students are expected to implement a random number generator and modify the executable file loader in xv6. The submission for each project is expected to demonstrate the module behavior comparable to relevant systems present in production grade OS, such as Linux.more » « less
-
Information flow control is a canonical approach to access control in systems, allowing administrators to assure confidentiality and integrity through restricting the flow of data. Decentralized Information Flow Control (DIFC) harnesses application-layer semantics to allow more precise and accurate mediation of data. Unfortunately, past approaches to DIFC have depended on dedicated instrumentation efforts or developer buy-in. Thus, while DIFC has existed for decades, it has seen little-to-no adoption in commodity systems; the requirement for complete redesign or retrofitting of programs has proven too high a barrier. In this work, we make the surprising observation that developers have already unwittingly performed the instrumentation efforts required for DIFC — application event logging, a software development best practice used for telemetry and debugging, often contains the information needed to identify application-layer event processes that DIFC mediates. We present T-difc, a kernel-layer reference monitor framework that leverages the insights of application event logs to perform precise decentralized flow control. T-difc identifies and extracts these application events as they are created by monitoring application I/O to log files, then references an administrator-specified security policy to assign data labels and mediate the flow of data through the system. To our knowledge, T-difc is the first approach to DIFC that does not require developer support or custom instrumentation. In a survey of 15 popular open source applications, we demonstrate that T-difc works seamlessly on a variety of popular open source programs while imposing negligible runtime overhead on realistic policies and workloads. Thus, T-difc demonstrates a transparent and non-invasive path forward for the dissemination of decentralized information flow controls.more » « less
-
Calzavara, Stefano ; Naumann, David (Ed.)more » « less
Availability is crucial to the security of distributed systems, but guaranteeing availability is hard, especially when participants in the system may act maliciously. Quorum replication protocols provide both integrity and availability: data and computation is replicated at multiple independent hosts, and a quorum of these hosts must agree on the output of all operations applied to the data. Unfortunately, these protocols have high overhead and can be difficult to calibrate for a specific application’s needs. Ideally, developers could use high-level abstractions for consensus and replication to write fault-tolerant code that is secure by construction. This paper presents Flow-Limited Authorization for Quorum Replication (FLAQR), a core calculus for building distributed applications with heterogeneous quorum replication protocols while enforcing end-to-end information security. Our type system ensures that well-typed FLAQR programs cannot fail (experience an unrecoverable error) in ways that violate their type-level specifications. We present noninterference theorems that characterize FLAQR’s confidentiality, integrity, and availability in the presence of consensus, replication, and failures, as well as a liveness theorem for the class of majority quorum protocols under a bounded number of faults. Additionally, we present an extension to FLAQR that supports secret sharing as a form of declassification and prove it preserves integrity and availability security properties.
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3453483.3454074
