Computer Science Technical Reports
Permanent URI for this collection
This is a collection of technical reports from the Cornell's Computer Science (CS) Department from the time period of 1968-2002. These reports are part of the NCSTRL collection of Computer Science Technical Reports.
For reports from 2003-present, see the Computing and Information Science Technical Reports Collection.
Browse
Recent Submissions
Item Tamperproof Provenance-Aware Storage for Mobile Ad Hoc NetworksAdams, Danny; Rubambiza, Gloire; Fiori, Pablo; Wang, Xinwen; Weatherspoon, Hakim; Van Renesse, Robbert (2020-12-08)This paper presents a middleware for providing a mobile ad hoc network with tamperproof provenance-aware storage, even when some fraction of devices can be Byzantine. Important considerations include fast propagation of updates, data consistency, and low power consumption. Leveraging entanglement techniques from blockchain protocols but carefully avoiding high power consumption and reliance on continuous network connectivity, we design new distributed data structures that can support useful distributed applications such as emergency response and IoT networks. Using both trace-based simulations and experiments with an Android-based prototype, we demonstrate the practicality of such a middleware.Item RIF: Reactive Information Flow LabelsKozyri, Elisavet; Schneider, Fred B. (2019-04-08)Restrictions that a reactive information flow (RIF) label imposes on a value are determined by the sequence of operations used to derive that value. This allows declassification, endorsement, and other forms of reclassification to be supported in a uniform way. Piecewise noninterference (PWNI) is introduced as a fitting security policy, because noninterference is not suitable. A type system is given for static enforcement of PWNI in programs that associate checkable classes of RIF labels with variables. Two checkable classes of RIF labels are described: RIF automata are general-purpose and based on finite-state automata; κ-labels concern confidentiality in programs that use cryptographic operations.Item Using Information Flow to Design an ISA that Controls Timing ChannelsZagieboylo, Drew; Suh, Gookwon Edward; Myers, Andrew C. (2019)Information-flow control (IFC) enforcing languages can provide high assurance that software does not leak information or allow an attacker to influence critical systems. IFC hardware description languages have also been used to design secure circuits that eliminate timing channels. However, there remains a gap between IFC hardware and software; these two components are built independently with no abstraction for how to compose their security guarantees. This paper presents a proposal for an instruction set architecture (ISA) that can provide the appropriate abstraction for joining hardware and software IFC mechanisms. Our ISA describes a RISC-V processor that tracks information-flow labels at run time and uses these labels to eliminate or mitigate timing channels. To make the ISA more practical, it allows constrained downgrading of information; it permits trading off security for performance; and still offers control primitives such as system calls. We prove timing-sensitive noninterference modulo downgrading and nonmalleability for programs executing our ISA. This involves novel restrictions on the mutability of labels beyond previous dynamic IFC systems. Furthermore, we define specific security conditions which correct hardware can implement to provide software-level security and sketch how such hardware may be designed and verified.Item Beyond Labels: Permissiveness for Dynamic Information Flow EnforcementKozyri, Elisavet; Schneider, Fred B.; Bedford, Andrew; Desharnais, Josée; Tawbi, Nadia (2019-02-28)Flow-sensitive labels used by dynamic enforcement mechanisms might themselves encode sensitive information, which can leak. Metalabels, employed to represent the sensitivity of labels, exhibit the same problem. This paper derives a new family of enforcers k-Enf , for k>1 that uses label chains, where each label defines the sensitivity of its predecessor. These enforcers satisfy Block-safe Noninterference (BNI), which proscribes leaks from observing variables, label chains, and blocked executions. Theorems in this paper characterize where longer label chains can improve the permissiveness of dynamic enforcement mechanisms that satisfy BNI. These theorems depend on semantic attributes---k-precise, k-varying, and k-dependent---of such mechanisms, as well as on initialization, threat model, and lattice size.Item X-Containers: Breaking Down Barriers to Improve Performance and Isolation of Cloud-Native ContainersShen, Zhiming; Sun, Zhen; Sela, Gur-Eyal; Bagdasaryan, Eugene; Delimitrou, Christina; Van Renesse, Robbert; Weatherspoon, Hakim (2018-08-29)“Cloud-native” container platforms, such as Kubernetes, have become an integral part of production cloud environments. One of the principles in designing cloud-native applications is called “Single Concern Principle”, which suggests that each container should handle a single responsibility well. Due to the resulting change in the threat model, process isolation within the container becomes redundant in most single-concerned containers, and inter-container isolation becomes increasingly important. In this paper, we propose a new exokernel-inspired architecture called X-Containers that improves both the security and the performance of cloud-native containers. We show that, through relatively minor modifications, the Xen hypervisor can serve as an exokernel, and Linux can be turned into a LibOS. Doing so results in a highly secure and efficient LibOS platform that, unlike other available LibOSes, supports binary compatibility and multicore processing. X-Containers have up to 27× higher raw system call throughput compared to Docker containers, while also significantly outperforming recent container platforms such as Google’s gVisor, Intel’s Clear Containers, as well as Library OSes like Unikernel and Graphene on web benchmarks.Item Security Results for SIRRTL, A Hardware Description Language for Information Flow SecurityFerraiuolo, Andrew (2017-12)This document establishes security results for SIRRTL, a secure variant of the FIRRTL intermediate language. We developed ChiselFlow, a variant of the Chisel hardware design language [1] for information flow security. ChiselFlow extends Chisel, a hardware description language embedded in Scala. ChiselFlow allows the hardeware designer to describe security policies about the hardware that are checked at design-time. Much like Chisel, ChiselFlow gains much of the expressive power of the rich host language, Scala. However, security enforcement is done by a small intermediate language called SIRRTL, so the trusted component of ChiselFlow is small. ChiselFlow emits SIRRTL, a variant of the FIRRTL intermediate language augmented with an information flow type system. ChiselFlow supports security policies that depend on the run-time values of signals, though these policies are checked purely at design-time by SIRRTL. In this document, we prove that well-typed SIRRTL modules enforce a timing safe variant of noninterference. We constructed the HyperFlow processor using ChiselFlow thereby establishing high assurance in the implementation of the processor.Item HyperFlow: A Processor Architecture for Timing-Safe Information-Flow SecurityFerraiuolo, Andrew; Zhao, Yuqi; Suh, G. Edward; Myers, Andrew C. (2018-05-01)This paper presents HyperFlow, a processor that enforces secure information flow, including control over timing channels. The design and implementation of HyperFlow offer security assurance because it is implemented using a security-typed hardware description language that enforces secure information flow. Unlike prior information-flow secured processors that aim to strictly enforce noninterference, HyperFlow supports complex information flow policies that can be configured at run time, and provides support for secure interprocess communication (IPC) and system calls. The architecture also offers a new model for process isolation in which memory protection is provided via information flow control with strong security assurance while allowing IPC and shared memory. HyperFlow is designed to support practical applications and system architectures. It therefore supports decentralized information flow mechanisms that allow controlled communication among mutually distrusting processes, mediated by dynamic, fine-grained labels. Static information- flow verification of such a complex processor architecture poses significant challenges, which require contributions in both the hardware architecture and the security type system. The paper discusses the architecture decisions that make the processor secure and describes a new secure HDL, named ChiselFlow, that allows these decisions to be verified in a lightweight way. The HyperFlow architecture is also prototyped on a fully-featured processor that offers a complete RISC-V instruction set, and is shown to have moderate overhead on area and performance.Item Undecidable Problems for Probabilistic Network ProgrammingKahn, David (2017-07-07)The software defined networking language NetKAT is able to verify many useful properties of networks automatically via a PSPACE decision procedure for program equality. However, for its probabilistic extension ProbNetKAT, no such decision procedure is known. We show that several potentially useful properties of ProbNetKAT are in fact undecidable, including emptiness of support intersection and certain kinds of distribution bounds and program comparisons. We do so by embedding the Post Correspondence Problem in ProbNetKAT via direct product expressions, and by directly embedding probabilistic finite automata.Item Flow-Limited AuthorizationArden, Owen (2017-01)Enforcing the confidentiality and integrity of information is critical in distributed applications. Production systems typically use some form of authorization mechanism to protect information, but these mechanisms do not typically provide end-to-end information security guarantees. Information flow control mechanisms provide end-to-end security, but their guarantees break down when trust relationships may change dynamically, a common scenario in production environments. This dissertation presents flow-limited authorization, a new foundation for enforcing information security. Flow-limited authorization is an approach to authorization in that it can be used to reason about whether a principal is permitted to perform an action. It is an approach to information flow control in that it can be used to reason about whether a flow of information is secure. This dissertation presents the theoretical foundation of this approach, the Flow-Limited Authorization Model (FLAM). FLAM uses a novel principal algebra that unifies authority and information flow policies and a logic for making secure authorization and information flow decisions. This logic ensures that such decisions cannot be influenced by attackers or leak confidential information. We embed the FLAM logic in a core programming model, the Flow-Limited Authorization Calculus (FLAC). FLAC programs selectively enable flows of information; the type system ensures that attackers cannot create unauthorized flows. A well-typed FLAC not only ensures proper authorization, but also secure information flow. The FLAC approach to secure programming is instantiated in \textsc{Flame}, a library and compiler plugin for enforcing flow-limited authorization in Haskell programs. Flame uses type-level constraints and monadic effects to statically enforce flow-limited authorization for Haskell programs in a modular way.