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.Item Lightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis (Technical Report)Ferraiuolo, Andrew; Xu, Rui; Zhang, Danfeng; Myers, Andrew C.; Suh, G. Edward (2017-01-29)Hardware-based mechanisms for software isolation are becoming increasingly popular, but implementing these mechanisms correctly has proved difficult, undermining the root of security. This work introduces an effective way to formally verify important properties of such hardware security mechanisms. In our approach, hardware is developed using a lightweight security-typed hardware description language (HDL) that performs static information flow analysis. We show the practicality of our approach by implementing and verifying a simplified but realistic multi-core prototype of the ARM TrustZone architecture. To make the security-typed HDL expressive enough to verify a realistic processor, we develop new type system features. Our experiments suggest that information flow analysis is efficient, and programmer effort is modest. We also show that information flow constraints are an effective way to detect hardware vulnerabilities, including several found in commercial processors.Item On Free ω-Continuous and Regular Ordered AlgebrasEsik, Zoltan; Kozen, Dexter (2016)Let E be a set of inequalities between finite Σ-terms. Let V_ω and V_r denote the varieties of all ω-continuous ordered Σ-algebras and regular ordered Σ-algebras satisfying E, respectively. We prove that the free V_r-algebra R(X) on generators X is the subalgebra of the corresponding free V_ω-algebra F_ω(X) determined by those elements of F_ω(X) denoted by the regular Σ-coterms. We actually establish this fact as a special case of a more general construction for families of algebras specified by syntactically restricted completeness and continuity properties. Thus our result is also applicable to ordered regular algebras of higher order.Item A Calculus for Flow-Limited Authorization: Technical ReportArden, Owen; Myers, Andrew C. (2016-09-13)Real-world applications routinely make authorization decisions based on dynamic computation. Reasoning about dynamically computed authority is challenging. Integrity of the system might be compromised if attackers can improperly influence the authorizing computation. Confidentiality can also be compromised by authorization, since authorization decisions are often based on sensitive data such as membership lists and passwords. Previous formal models for authorization do not fully address the security implications of permitting trust relationships to change, which limits their ability to reason about authority that derives from dynamic computation. Our goal is a way to construct dynamic authorization mechanisms that do not violate confidentiality or integrity.Item Block-safe Information Flow ControlKozyri, Elisavet; Desharnais, Josée; Tawbi, Nadia (2016-08-09)Flow-sensitive dynamic enforcement mechanisms for information flow labels offer increased permissiveness. However, these mechanisms may leak sensitive information when deciding to block insecure executions. When enforcing two labels (e.g., secret and public), sensitive information is leaked from the context in which this decision is taken. When enforcing arbitrary labels, additional sensitive information is leaked from the labels involved in the decision to block an execution. We give examples where, contrary to a common belief, a mechanism designed to enforce two labels may not be able to enforce arbitrary labels, due to this additional leakage. In fact, it is not trivial to design a dynamic enforcement that offers increased permissiveness, handles multiple labels, and does not introduce information leakage due to blocking insecure executions. In this paper, we present a dynamic enforcement mechanism of information flow labels that has all these three attributes. Our mechanism is not purely dynamic, since it uses a light-weight, on-the-fly, static analysis of untaken branches. We prove that the set of all normally terminated and blocked traces of a program, which is executed under our mechanism, satisfies noninterference, against principals that make observations throughout execution.Item JRIF: Reactive Information Flow Control for JavaKozyri, Elisavet; Arden, Owen; Myers, Andrew C.; Schneider, Fred B. (2016-02-12)A reactive information flow (RIF) automaton for a value v specifies (i) allowed uses for v and (ii) the RIF automaton for any value that might be directly or indirectly derived from v. RIF automata thus specify how transforming a value alters how the result might be used. Such labels are more expressive than existing approaches for controlling downgrading. We devised a type system around RIF automata and incorporated it into Jif, a dialect of Java that supports a classic form of labels for information flow. By implementing a compiler for the resulting JRIF language, we demonstrate how easy it is to replace a classic information-flow type system by a more expressive RIF-based type system. We programmed two example applications in JRIF, and we discuss insights they provide into the benefits of RIF-based security labels.Item Flow-Limited AuthorizationArden, Owen; Liu, Jed; Myers, Andrew (2015-05-08)Because information flow control mechanisms often rely on an underlying authorization mechanism, their security guarantees can be subverted by weaknesses in authorization. Conversely, the security of authorization can be subverted by information flows that leak information or that influence the delegation of authority among principals. We argue that interactions between information flow and authorization create security vulnerabilities that have not been fully identified or addressed in prior work. We explore how the security of decentralized information flow control (DIFC) is affected by three aspects of its underlying authorization mechanism: first, delegation of authority between principals; second, revocation of previously delegated authority; third, information flows created by the authorization mechanisms themselves. It is no surprise that revocation poses challenges, but we show that even delegation is problematic because it enables unauthorized downgrading. Our solution is a new security model, the Flow-Limited Authorization Model (FLAM), which offers a new, integrated approach to authorization and information flow control. FLAM ensures robust authorization, a novel security condition for authorization queries that ensures attackers cannot influence authorization decisions or learn confidential trust relationships. We discuss our prototype implementation and its algorithm for proof search.Item A Linear List Merging AlgorithmHopcroft, John E.; Ullman, Jeffrey D. (2008-05-14T13:42:16Z)A linear list merging algorithm and its analysis is presented. Starting with n lists, each containing a single element, the algorithm will execute an arbitrary sequence of requests to merge lists and to find the name of the list currently containing a given element. If the length of the sequence of requests is bounded by a constant times n, then the execution time of the algorithm on a random access computer is bounded by a constant times n.Item On the Modelling Power of Petri NetsMeiling, Erik (Cornell University, 1979-12)The behavior of a Petri net is expressed as a formal language. Certain families of Petri net languages are characterized by propositions similar to the classical pumping theorems. The results are used to give examples of behaviors that cannot be expressed by languages in these families.Item Cand and Cor Before and Then or Else in AdaGries, David (Cornell University, 1979-11)NO ABSTRACT SUPPLIEDItem A Proof Technique for Communicating Sequential Processes(With an Example)Levin, Gary Marc (Cornell University, 1979-11)We present proof rules for an extension of the Communicating Sequential Processes proposed by Hoare. The send and receive statements are treated symmetrically, simplifying the rules and allowing send to appear in guards. An example is given to explain the use of the technique. This is an outline of a substantial part of a PhD thesis that is expected to be completed in June 1980.