Steve Zdancewic's Publications
Copyright Information
Journal Articles
[1] Peng Li and Steve Zdancewic. Arrows for Secure Information Flow. Theoretical Computer Science, 411(19):1974-1994, 2010. [ PDF ]
This paper presents an embedded security sublanguage for enforcing information- flow policies in the standard Haskell programming language. The sublanguage pro- vides useful information-flow control mechanisms including dynamic security lat- tices, run-time code privileges and declassification all without modifying the base language. This design avoids the redundant work of producing new languages, low- ers the threshold for adopting security-typed languages, and also provides great flexibility and modularity for using security-policy frameworks.

The embedded security sublanguage is designed using a standard combinator in- terface called arrows. Computations constructed in the sublanguage have static and explicit control-flow components, making it possible to implement information-flow control using static-analysis techniques at run time, while providing strong secu- rity guarantees. This paper presents a formal proof that our embedded sublanguage provides noninterference, a concrete Haskell implementation and an example appli- cation demonstrating the proposed techniques.

[2] Stephen Tse and Steve Zdancewic. Run-time principals in information-flow type systems. Transactions on Programming Languages and Systems, 30(1):6, 2008. [ PDF ]
Information-flow type systems are a promising approach for enforcing strong end-to-end confidentiality and integrity policies. Such policies, however, are usually specified in terms of static information-data is labeled _high_ or _low_ security at compile time. In practice, the confidentiality of data may depend on information available only while the system is running. This paper studies language support for _run-time principals_, a mechanism for specifying security policies that depend on which principals interact with the system. We establish the basic property of noninterference for programs written in such language, and use run-time principals for specifying run-time authority in downgrading mechanisms such as declassification. In addition to allowing more expressive security policies, run-time principals enable the integration of language-based security mechanisms with other existing approaches such as Java stack inspection and public key infrastructures. We sketch an implementation of run-time principals via public keys such that principal delegation is verified by certificate chains.

[3] Jay Ligatti, David Walker, and Steve Zdancewic. A Type-theoretic Interpretation of Pointcuts and Advice. Science of Computer Programming: Special Issue on Foundations of Aspect-Oriented Programming, pages 240-266, 2006. [ PDF ]
This paper defines the semantics of MinAML, an idealized aspect-oriented programming language, by giving a type-directed translation from a user-friendly external language to a compact, well-defined core language. We argue that our framework is an effective way to give semantics to aspect-oriented programming languages in general because the translation eliminates shallow syntactic differences between related constructs and permits definition of a simple and elegant core language.

The core language extends the simply-typed lambda calculus with two central new abstractions: explicitly labeled program points and first-class advice. The labels serve both to trigger advice and to mark continuations that the advice may return to. These constructs are defined orthogonally to the other features of the language and we show that our abstractions can be used in both functional and object-oriented contexts. We prove Preservation and Progress lemmas for our core language and show that the translation from MinAML source into core is type-preserving. We also consider several extensions to our basic framework including a general mechanism for analyzing the current call stack.

[4] Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic. Enforcing Robust Declassification and Qualified Robustness. Journal of Computer Security, 14(2):157-196, 2006. [ PDF ]
Noninterference requires that there is no information flow from sensitive to public data in a given system. However, many systems release sensitive information as part of their intended function and therefore violate noninterference. To control information flow while permitting information release, some systems have a downgrading or declassification mechanism, but this creates the danger that it may cause unintentional information release. This paper shows that a robustness property can be used to characterize programs in which declassification mechanisms cannot be controlled by attackers to release more information than intended. It describes a simple way to provably enforce this robustness property through a type-based compile-time program analysis. The paper also presents a generalization of robustness that supports upgrading (endorsing) data integrity.

[5] Steve Zdancewic and Andrew C. Myers. Secure Information Flow via Linear Continuations. Higher Order and Symbolic Computation, 15(2/3):209-234, 2002. [ PDF  PS ]
Security-typed languages enforce secrecy or integrity policies by type-checking. This paper investigates continuation-passing style (CPS) as a means of proving that such languages enforce noninterference and as a first step towards understanding their compilation. We present a low-level, secure calculus with higher-order, imperative features and linear continuations.

Linear continuations impose a stack discipline on the control flow of programs. This additional structure in the type system lets us establish a strong information-flow security property called noninterference. We prove that our CPS target language enjoys the noninterference property and we show how to translate secure high-level programs to this low-level language. This noninterference proof is the first of its kind for a language with higher-order functions and state.

[6] Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. Secure Program Partitioning. Transactions on Computer Systems, 20(3):283-328, 2002. [ PDF  PS ]
This paper presents secure program partitioning, a language-based technique for protecting confidential data during computation in distributed systems containing mutually untrusted hosts. Confidentiality and integrity policies can be expressed by annotating programs with security types that constrain information flow; these programs can then be partitioned automatically to run securely on heterogeneously trusted hosts. The resulting communicating subprograms collectively implement the original program, yet the system as a whole satisfies the security requirements of participating principals without requiring a universally trusted host machine. The experience in applying this methodology and the performance of the resulting distributed code suggest that this is a promising way to obtain secure distributed computation.

This article is an expanded version of the published paper “Untrusted Hosts and Confidentiality: Secure Program Partitioning”. The main difference between the two is Appendix A, which contains a correctness proof for the control-transfer protocols described in Section 5.

[7] Dan Grossman, Greg Morrisett, and Steve Zdancewic. Syntactic Type Abstraction. Transactions on Programming Languages and Systems, 22(6):1037-1080, November 2000. [ PDF  PS ]
Software developers often structure programs in such a way that different pieces of code constitute distinct principals. Types help define the protocol by which these principals interact. In particular, abstract types allow a principal to make strong assumptions about how well-typed clients use the facilities that it provides. We show how the notions of principals and type abstraction can be formalized within a language. Different principals can know the implementation of different abstract types. We use additional syntax to track the flow of values with abstract types during the evaluation of a program and demonstrate how this framework supports syntactic proofs (in the style of subject reduction) for type-abstraction properties. Such properties have traditionally required semantic arguments; using syntax avoids the need to build a model for the language. We present various typed lambda calculi with principals, including versions that have mutable state and recursive types.

Invited Papers
[1] Steve Zdancewic. Challenges for Information-flow Security. In Proceedings of the 1st International Workshop on the Programming Language Interference and Dependence (PLID'04), 2004. (5 pages). [ PDF ]
[2] Steve Zdancewic. A Type System for Robust Declassification. In Proceedings of the Nineteenth Conference on the Mathematical Foundations of Programming Semantics (MFPS). Electronic Notes in Theoretical Computer Science, March 2003. (16 pages). [ PDF  PS ]
Language-based approaches to information security have led to the development of security type systems that permit the programmer to describe confidentiality policies on data. Security type systems are usually intended to enforce noninterference, a property that requires that high-security information not affect low-security computation. However, in practice, noninterference is often too restrictive-the desired policy does permit some information leakage.

To compensate for the strictness of noninterference, practical approaches include some mechanism for declassifying high-security information. But such declassification is potentially dangerous, and its use should be restricted to prevent unintended information leaks. Zdancewic and Myers previously introduced the notion of robust declassification in an attempt to capture the desired restrictions on declassification, but that work did not propose a method for determining when a program satisfies the robust declassification condition.

This paper motivates robust declassification and shows that a simple change to a security type system can enforce it. The idea is to extend the lattice of security labels to include integrity constraints as well as confidentiality constraints and then require that the decision to perform a declassification have high integrity.

Conference and Selective Workshop Papers
[1] Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A Core Quantitative Coeffect Calculus. In Proc. of the 23rd European Symposium on Programming (ESOP), volume 8410, pages 351-370, 2014. [ PDF ]
Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. Its resource-awareness arises from the distinction between linear, single-use data and non-linear, reusable data. The latter is marked by the so-called exponential modality, which, from the categorical viewpoint, is a (monoidal) comonad.

Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this work, we present a language lrPCF inspired by a generalized interpretation of the exponential modality. In lrPCF the exponential modality carries a label-an element of a semiring R-that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis.

[2] Santosh Nagarakatte, Milo M K Martin, and Steve Zdancewic. Hardware-Accelerated Compiler-Based Pointer Checking. In International Symposium on Code Generation and Optimization (CGO), 2014. (to appear).
[3] Santosh Nagarakatte, Milo M K Martin, and Steve Zdancewic. Hardware-enforced Comprehensive Memory Safety. IEEE MICRO's "Top Picks of Architecture Conferences of 2012" Issue (Micro Top Picks'2013), May/June 2013. [ PDF ]
The lack of memory safety in languages such as C and C++ is a root source of exploitable security vulnerabilities. This article presents Watchdog, a hardware approach that eliminates such vulnerabilities by enforcing comprehensive memory safety. Inspired by prior software-only mechanisms, Watchdog maintains bounds and identifier metadata with pointers, propagates them on pointer operations, and checks them on pointer dereferences. Checking this bounds and identifier metadata provides both precise, byte-granularity buffer-overflow protection and protection from use-after-free errors, even in the presence of reallocations. Watchdog stores pointer metadata in a disjoint shadow space to provide comprehensive protection and ensure compatibility with existing code. To streamline implementation and reduce runtime overhead, Watchdog uses micro-operations to implement metadata access and checking, eliminates metadata copies via a register renaming scheme, and uses a dedicated identifier cache to reduce checking overhead.

[4] Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, and Steve Zdancewic. Ironclad C++: A Library-Augmented Type-Safe Subset of C++. In Proceedings of the 28th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA), 2013. [ PDF ]
The C++ programming language remains widely used, despite inheriting many unsafe features from C-features that often lead to failures of type or memory safety that manifest as buffer overflows, use-after-free vulnerabilities, or abstraction violations. Malicious attackers can exploit such violations to compromise application and system security.

This paper introduces Ironclad C++, an approach to bringing the benefits of type and memory safety to C++. Ironclad C++ is, in essence, a library-augmented, type-safe subset of C++. All Ironclad C++ programs are valid C++ programs that can be compiled using standard, off-the-shelf C++ compilers. However, not all valid C++ programs are valid Ironclad C++ programs: a syntactic source-code validator statically prevents the use of unsafe C++ features. To enforce safety properties that are difficult to check statically, Ironclad C++ applies dynamic checks via templated “smart pointer” classes.

Using a semi-automatic refactoring tool, we have ported nearly 50K lines of code to Ironclad C++. These benchmarks incur a performance overhead of 12% on average, compared to the original unsafe C++ code.

[5] Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Formal Verification of SSA-Based Optimizations for LLVM. In Proc. 2013 ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), 2013. [ PDF ]
Modern compilers, such as LLVM and GCC, use a static single assignment (SSA) intermediate representation (IR) to simplify and enable many advanced optimizations. However, formally verifying the correctness of SSA-based optimizations is challenging because SSA properties depend on a function's entire control-flow graph.

This paper addresses this challenge by developing a proof technique for proving SSA-based program invariants and compiler optimizations. We use this technique in the Coq proof assistant to create mechanized correctness proofs of several “micro” transformations that form the building blocks for larger SSA optimizations. To demonstrate the utility of this approach, we formally verify a variant of LLVM's transformation in , a Coq-based formal semantics of the LLVM IR. The extracted implementation generates code with performance comparable to that of LLVM's unverified implementation.

[6] Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Watchdog: Hardware for Safe and Secure Manual Memory Management and Full Memory Safety. In Proceedings of the 39th International Symposium on Computer Architecture (ISCA), June 2012. [ PDF ]
Languages such as C and C++ use unsafe manual memory management, allowing simple bugs (i.e., accesses to an object after deallocation) to become the root cause of exploitable security vulnerabilities. This paper proposes Watchdog, a hardware-based approach for ensuring safe and secure manual memory management. Inspired by prior software-only proposals, Watchdog generates a unique identifier for each memory allocation, associates these identifiers with pointers, and checks to ensure that the identifier is still valid on every memory access. This use of identifiers and checks enables Watchdog to detect errors even in the presence of reallocations. Watchdog stores these pointer identifiers in a disjoint shadow space to provide comprehensive protection and ensure compatibility with existing code. To streamline the implementation and reduce runtime overhead: Watchdog (1) uses micro-ops to access metadata and perform checks, (2) eliminates metadata copies among registers via modified register renaming, and (3) uses a dedicated metadata cache to reduce checking overhead. Furthermore, this paper extends Watchdog's mechanisms to detect bounds errors, thereby providing full hardware-enforced memory safety at low overheads.

[7] Jianzhou Zhao and Steve Zdancewic. Mechanized Verification of Computing Dominators for Formalizing Compilers. In The Second International Conference on Certified Programs and Proofs (CPP), Lecture Notes in Computer Science, pages 27-42, 2012. [ PDF ]
One prerequisite to the formal verification of modern compilers is to formalize computing dominators, which enable SSA forms, advanced optimizations, and analysis. This paper provides an abstract specification of dominance analysis that is sufficient for formalizing modern compilers; it describes a certified implementation and instance of the specification that is simple to design and reason about, and also reasonably efficient. The paper also presents applications of dominance analysis: an SSA-form type checker, verifying SSA-based optimizations, and constructing dominator trees. This development is a part of the Vellvm project. All proofs and implementation have been carried out in Coq.

[8] Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In Proc. of the ACM Symposium on Principles of Programming Languages (POPL), 2012. [ PDF ]
This paper presents Vellvm (verified LLVM), a framework for reasoning about programs expressed in LLVM's intermediate representation and transformations that operate on it. Vellvm provides a mechanized formal semantics of LLVM's intermediate representation, its type system, and properties of its SSA form. The framework is built using the Coq interactive theorem prover. It includes multiple operational semantics and proves relations among them to facilitate different reasoning styles and proof techniques.

To validate Vellvm's design, we extract an interpreter from the Coq formal semantics that can execute programs from LLVM test suite and thus be compared against LLVM reference implementations. To demonstrate Vellvm's practicality, we formalize and verify a previously proposed transformation that hardens C programs against spatial memory safety violations. Vellvm's tools allow us to extract a new, verified implementation of the transformation pass that plugs into the real LLVM infrastructure; its performance is competitive with the non-verified, ad-hoc original.

[9] Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic. Generative Type Abstraction and Type-level Computation. In Proc. of the ACM Symposium on Principles of Programming Languages (POPL), 2011. [ PDF ]
Modular languages support generative type abstraction, ensuring that an abstract type is distinct from its representation, except inside the implementation where the two are synonymous. We show that this well-established feature is in tension with the non-parametric features of newer type systems, such as indexed type families and GADTs. In this paper we solve the problem by using kinds to distinguish between parametric and non-parametric contexts. The result is directly applicable to Haskell, which is rapidly developing support for type-level computation, but the same issues should arise whenever generativity and non-parametric features are combined.

[10] Jianzhou Zhao, Qi Zhang, and Steve Zdancewic. Relational Parametricity for Polymorphic Linear Lambda Calculus. In Proceedings of the Eighth ASIAN Symposium on Programming Languages and Systems (APLAS), 2010. [ PDF ]
This paper presents a novel syntactic logical relation for a polymorphic linear lambda-calculus that treats all types as linear and introduces the constructor ! to account for intuitionistic terms, and Fo-an extension of System F that uses kinds to distinguish linear from intuitionistic types. We define a logical relation for open values under both open linear and intuitionistic contexts, then extend it for open terms with evaluation and open relation substitutions. Relations that instantiate type quantifiers are for open terms and types. We demonstrate the applicability of this logical relation through its soundness with respect to contextual equivalence, along with free theorems for linearity that are difficult to achieve by closed logical relations. When interpreting types on only closed terms, the model defaults to a closed logical relation that is both sound and complete with respect to contextual equivalence and is sufficient to reason about isomorphisms of type encodings. All of our results have been mechanically verified in Coq.

[11] Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. CETS: Compiler-Enforced Temporal Safety for C. In Proceedings of the ACM International Symposium on Memory Management (ISMM), 2010. [ PDF ]
Temporal memory safety errors, such as dangling pointer dereferences and double frees, are a prevalent source of software bugs in unmanaged languages such as C. Existing schemes that attempt to retrofit temporal safety for such languages have high runtime overheads and/or are incomplete, thereby limiting their effectiveness as debugging aids. This paper presents CETS, a compile-time transformation for detecting all violations of temporal safety in C programs. Inspired by existing approaches, CETS maintains a unique identifier with each object, associates this metadata with the pointers in a disjoint metadata space to retain memory layout compatibility, and checks that the object is still allocated on pointer dereferences. A formal proof shows that this is sufficient to provide temporal safety even in the presence of arbitrary casts if the program contains no spatial safety violations. Our CETS prototype employs both temporal check removal optimizations and traditional compiler optimizations to achieve a runtime overhead of just 48% on average. When combined with a spatial-checking system, the average overall overhead is 116% for complete memory safety.

[12] Karl Mazurak and Steve Zdancewic. Lolliproc: to Concurrency from Classical Linear Logic via Curry-Howard and Control. In Proc. of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2010. [ PDF ]
While many type systems based on the intuitionistic fragment of linear logic have been proposed, applications in programming languages of the full power of linear logic-including double-negation elimination-have remained elusive. Meanwhile, linearity has been used in many type systems for concurrent programs-e.g., session types-which suggests applicability to the problems of concurrent programming, but the ways in which linearity has interacted with concurrency primitives in lambda calculi have remained somewhat ad-hoc. In this paper we connect classical linear logic and concurrent functional programming in the language Lolliproc, which provides simple primitives for concurrency that have a direct logical interpretation and that combine to provide the functionality of session types. Lolliproc features a simple process calculus “under the hood” but hides the machinery of processes from programmers. We illustrate Lolliproc by example and prove soundness, strong normalization, and confluence results, which, among other things, guarantees freedom from deadlocks and race conditions.

[13] Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and Steve Zdancewic. Reactive Noninterference. In ACM Computer and Communications Security Conference (CCS), 2009. [ PDF ]
Many programs operate reactively-patiently waiting for user input, running for a while producing output, and eventually returning to a state where they are ready to accept another input (or occasionally diverging). When a reactive program communicates with multiple parties, we would like to be sure that it can be given secret information by one without leaking it to others.

Motivated by web browsers and client-side web applications, we explore definitions of noninterference for reactive programs and identify two of special interest-one corresponding to termination-insensitive noninterference for a simple sequential language, the other to termination-sensitive noninterference. We focus on the former and develop a proof technique for showing that program behaviors are secure according to this definition. To demonstrate the viability of the approach, we define a simple reactive language with an information-flow type system and apply our proof technique to show that well-typed programs are secure.

[14] J. Nathan Foster, Benjamin C. Pierce, and Steve Zdancewic. Updatable Security Views. In Proc. of 22nd IEEE Computer Security Foundations Symposium (CSF), 2009. [ PDF ]
Security views are a flexible and effective mechanism for controlling access to confidential information. Rather than allowing untrusted users to access source data directly, they are instead provided with a restricted view, from which all confidential information has been removed. The program that generates the view effectively embodies a confidentiality policy for the underlying source data. However, this approach has a significant drawback: it prevents users from updating the data in the view.

To address the “view update problem” in general, a number of bidirectional languages have been proposed. Programs in these languages-often called lenses-can be run in two directions: read from left to right, they map sources to views; from right to left, they map updated views back to updated sources. However, existing bidirectional languages do not deal adequately with security. In particular, they do not provide a way to ensure the integrity of source data as it is manipulated by untrusted users of the view.

We propose a novel framework of secure lenses that addresses these shortcomings. We enrich the types of basic lenses with equivalence relations capturing notions of confidentiality and integrity, and formulate the essential security conditions as non-interference properties. We then instantiate this framework in the domain of string transformations, developing syntax for bidirectional string combinators with security-annotated regular expressions as their types.

[15] Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. SoftBound: Highly Compatible and Complete Spatial Memory Safety for C. In Proc. 2009 ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), 2009. [ PDF ]
The serious bugs and security vulnerabilities facilitated by C/C++'s lack of bounds checking are well known, yet C and C++ remain in widespread use. Unfortunately, C's arbitrary pointer arithmetic, conflation of pointers and arrays, and programmer-visible memory layout make retrofitting C/C++ with spatial safety guarantees extremely challenging. Existing approaches suffer from incompleteness, have high runtime overhead, or require non-trivial changes to the C source code. Thus far, these deficiencies have prevented widespread adoption of such techniques.

This paper proposes SoftBound, a compile-time transformation for enforcing spatial safety of C. Inspired by HardBound, a previously proposed hardware-assisted approach, SoftBound similarly records base and bound information for every pointer as disjoint metadata. This decoupling enables SoftBound to provide spatial safety without requiring changes to C source code. Unlike HardBound, SoftBound is a software-only approach and performs metadata manipulation only when loading or storing pointer values. A formal proof shows that this is sufficient to provide spatial safety even in the presence of arbitrary casts. SoftBound's full checking mode provides complete spatial violation detection with 67% runtime overhead on average. To further reduce overheads, SoftBound has a store-only checking mode that successfully detects all the security vulnerabilities in a test suite at the cost of only 22% runtime overhead on average.

[16] Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. AURA: A Programming Language for Authorization and Audit. In Proc. of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP), Victoria, British Columbia, Canada, September 2008. [ PDF ]
This paper presents AURA, a programming language for access control that treats ordinary programming constructs (e.g., integers and recursive functions) and authorization logic constructs (e.g., principals and access control policies) in a uniform way. AURA is based on polymorphic DCC and uses dependent types to permit assertions that refer directly to AURA values while keeping computation out of the assertion level to ensure tractability. The main technical results of this paper include fully mechanically verified proofs of the decidability and soundness for AURA's type system, and a prototype typechecker and interpreter.

[17] Joe Devietti, Colin Blundell, Milo M.K. Martin, and Steve Zdancewic. HardBound: Architectural Support for Spatial Safety of the C Programming Language. In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March 2008. [ PDF ]
The C programming language is at least as well known for its absence of spatial memory safety guarantees (i.e., lack of bounds checking) as it is for its high performance. C's unchecked pointer arithmetic and array indexing allow simple programming mistakes to lead to erroneous executions, silent data corruption, and security vulnerabilities. Many prior proposals have tackled enforcing spatial safety in C programs by checking pointer and array accesses. However, existing software-only proposals have significant drawbacks that may prevent wide adoption, including: unacceptably high runtime overheads, lack of completeness, incompatible pointer representations, or need for non-trivial changes to existing C source code and compiler infrastructure.

Inspired by the promise of these software-only approaches, this paper proposes a hardware bounded pointer architectural primitive that supports cooperative hardware/software enforcement of spatial memory safety for C programs. This bounded pointer is a new hardware primitive datatype for pointers that leaves the standard C pointer representation intact, but augments it with bounds information maintained separately and invisibly by the hardware. The bounds are initialized by the software, and they are then propagated and enforced transparently by the hardware, which automatically checks a pointer's bounds before it is dereferenced. One mode of use requires instrumenting only malloc, which enables enforcement of per-allocation spatial safety for heap-allocated objects for existing binaries. When combined with simple intra-procedural compiler instrumentation, hardware bounded pointers enable a low-overhead approach for enforcing complete spatial memory safety in unmodified C programs.

[18] Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic. Evidence-based Audit. In Proc. of 21st IEEE Computer Security Foundations Symposium (CSF), pages 177-191. IEEE Computer Society Press, 2008. [ PDF ]
Authorization logics provide a principled and flexible approach to specifying access control policies. One of their compelling benefits is that a proof in the logic is evidence that an access-control decision has been made in accordance with policy. Using such proofs for auditing reduces the trusted computing base and enables the ability to detect flaws in complex authorization policies. Moreover, the proof structure is itself useful, because proof normalization can yield information about the relevance of policy statements. Untrusted, but well-typed, applications that access resources through an appropriate interface must obey the access control policy and create proofs useful for audit.

This paper presents AURA, an authorization logic based on a dependently-typed variant of DCC and proves the metatheoretic properties of subject-reduction and normalization. It shows the utility of proof-based auditing in a number of examples and discusses several pragmatic issues that must be addressed in this context.

[19] Jeffrey A. Vaughan and Steve Zdancewic. A Cryptographic Decentralized Label Model. In IEEE 2007 Symposium on Security and Privacy (Oakland), pages 192-206, 2007. [ PDF  PS ]
Information-flow security policies are an appealing way of specifying confidentiality and integrity policies in information systems. Most previous work on language-based security has assumed that programs run in a closed, managed environment and that they use potentially unsafe constructs, such as declassification, to interface to external communication channels, perhaps after encrypting data to preserve its confidentiality. This situation is unsatisfactory for systems that need to communicate over untrusted channels or use untrusted persistent storage, since the connection between the cryptographic mechanisms used in the untrusted environment and the abstract security labels used in the trusted language environment is ad hoc and unclear.

This paper addresses this problem in three ways: First, it presents a simple, security-typed language with a novel mechanism called packages that provides an abstract means for creating opaque objects and associating them with security labels; well-typed programs in this language enforce noninterference. Second, it shows how to implement these packages using public-key cryptography. This implementation strategy uses a variant of Myers and Liskov's decentralized label model, which supports a rich label structure in which mutually distrusting data owners can specify independent confidentiality and integrity requirements. Third, it demonstrates that this implementation of packages is sound with respect to Dolev-Yao style attackers-such an attacker cannot determine the contents of a package without possessing the appropriate keys, as determined by the security label on the package.

[20] Peng Li and Steve Zdancewic. Combining Events And Threads For Scalable Network Services. In Proc. 2007 ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), pages 189-199, 2007. [ PS ]
This paper proposes to combine two seemingly opposed programming models for building massively concurrent network services: the event-driven model and the multithreaded model. The result is a hybrid design that offers the best of both worlds-the ease of use and expressiveness of threads and the flexibility and performance of events.

This paper shows how the hybrid model can be implemented entirely at the application level using concurrency monads in Haskell, which provides type-safe abstractions for both events and threads. This approach simplifies the development of massively concurrent software in a way that scales to real-world network services. The Haskell implementation supports exceptions, symmetrical multiprocessing, software transactional memory, asynchronous I/O mechanisms and application-level network protocol stacks. Experimental results demonstrate that this monad-based approach has good performance: the threads are extremely lightweight (scaling to ten million threads), and the I/O performance compares favorably to that of Linux NPTL.

[21] Rajeev Alur, Pavol Černý, and Steve Zdancewic. Preserving Secrecy under Refinement. In Proc. of 33rd International Colloquium on Automata, Languages and Programming (ICALP), pages 107-118, 2006. [ PDF ]
We propose a general framework of secrecy and preservation of secrecy for labeled transition systems. Our definition of secrecy is parameterized by the distinguishing power of the observer, the properties to be kept secret, and the executions of interest, and captures a multitude of definitions in the literature. We define a notion of secrecy preserving refinement between systems by strengthening the classical trace-based refinement so that the implementation leaks a secret only when the specification also leaks it. We show that secrecy is in general not definable in mu-calculus, and thus not expressible in specification logics supported by standard model-checkers. However, we develop a simulation-based proof technique for establishing secrecy preserving refinement. This result shows how existing refinement checkers can be used to show correctness of an implementation with respect to a specification.

[22] Peng Li and Steve Zdancewic. Encoding Information Flow in Haskell. In Proc. of 19th IEEE Computer Security Foundations Workshop (CSFW), pages 16-27. IEEE Computer Society Press, 2006. [ PDF ]
This paper presents an embedded security sublanguage for enforcing information-flow policies in the standard Haskell programming language. The sublanguage provides useful information-flow control mechanisms including dynamic security lattices, run-time code privileges and declassification, without modifying the base language. This design avoids the redundant work of producing new languages, lowers the threshold for adopting security-typed languages, and also provides great flexibility and modularity for using security-policy frameworks. The embedded security sublanguage is designed using a standard combinator interface called arrows. Computations constructed in the sublanguage have static and explicit control-flow components, making it possible to implement information-flow control using static-analysis techniques at run time, while providing strong security guarantees. This paper presents a concrete Haskell implementation and an example application demonstrating the proposed techniques.

[23] Nikhil Swamy, Michael Hicks, Stephen Tse, and Steve Zdancewic. Managing Policy Updates in Security-Typed Languages. In Proc. of 19th IEEE Computer Security Foundations Workshop (CSFW), pages 202-216. IEEE Computer Society Press, 2006. [ PDF ]
This paper presents RX, a new security-typed programming language with features intended to make the management of information-flow policies more practical. Security labels in RX, in contrast to prior approaches, are defined in terms of owned roles, as found in the RT role-based trust-management framework. Role-based security policies allow flexible delegation, and our language RX provides constructs through which programs can robustly update policies and react to policy updates dynamically. Our dynamic semantics use statically verified transactions to eliminate illegal information flows across updates, which we call transitive flows. Because policy updates can be observed through dynamic queries, policy updates can potentially reveal sensitive information. As such, RX considers policy statements themselves to be potentially confidential information and subject to information-flow metapolicies.

[24] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized Metatheory for the Masses: The POPLMark Challenge. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pages 50-65, 2005. [ PDF ]
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs?

We propose an initial set of benchmarks for measuring progress in this area. Based on the metatheory of System F-Sub, a typed lambda-calculus with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research.

[25] Stephen Tse and Steve Zdancewic. Designing a Security-typed Language with Certificate-based Declassification. In Proc. of the 14th European Symposium on Programming (ESOP), volume 3444, pages 279-294, 2005. [ PDF ]
This paper presents a calculus that supports information-flow security policies and certificate-based declassification. The decentralized label model and its downgrading mechanisms are concisely expressed in the polymorphic lambda calculus with subtyping (System F-Sub). We prove a conditioned version of the noninterference theorem such that authorization for declassification is justified by digital certificates from public-key infrastructures.

[26] Peng Li and Steve Zdancewic. Practical Information-flow Control in Web-based Information Systems. In Proc. of 18th IEEE Computer Security Foundations Workshop (CSFW), pages 2-15, 2005. [ PDF ]
This paper presents a practical application of language-based information-flow control, namely, a domain-specific web scripting language designed for interfacing with databases. The primary goal is to provide strong enforcement of confidentiality and integrity policies: confidential data can be released only in permitted ways and trustworthy data must result from expected computations or conform to expected patterns. Such security policies are specified in the database layer and statically enforced for the rest of the system in an end-to-end fashion.

In contrast with existing web-scripting languages, which provide only ad hoc mechanisms for information security, the scripting language described here uses principles based on the well-studied techniques in information-flow type systems. However, because web scrips often need to downgrade confidential data and manipulate untrusted user input, they require practical and convenient ways of downgrading secure data. To achieve this goal, the language allows safe downgrading according to downgrading policies specified by the programmer. This novel, pattern-based approach provides a practical instance of recent work on delimited release and relaxed noninterference and extends that work by accounting for integrity policies.

[27] Peng Li and Steve Zdancewic. Downgrading Policies and Relaxed Noninterference. In Proc. 32nd ACM Symp. on Principles of Programming Languages (POPL), pages 158-170, January 2005. [ PDF ]
In traditional information-flow type systems, the security policy is often formalized as noninterference properties. However, noninterference alone is too strong to express security properties useful in practice. If we allow downgrading in such systems, it is challenging to formalize the security policy as an extensional property of the system.

This paper presents a generalized framework of downgrading policies. Such policies can be specified in a simple and tracable language and can be statically enforced by mechanisms such as type systems. The security guarantee is then formalized as a concise extensional property using program equivalences. This relaxed noninterference generalizes traditional pure noninterference and precisely characterizes the information released due to downgrading.

[28] Peng Li and Steve Zdancewic. Advanced Control Flow in Java Card Programming. In Proceedings of the 2004 ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), pages 165-174, June 2004. [ PDF ]
Java Card technology simplifies the development of smart card applications by providing a high-level programming language similar to Java. However, the master-slave programming model used in current Java Card platform creates control flow difficulties when writing complex card programs, making it inconvenient, tedious, and error-prone to implement Java Card applications. This paper examines these drawbacks of the master-slave model and proposes a concurrent thread model for developing future Java Card programs, which is much closer to conventional Java network programming. This paper also presents a code translation algorithm and a corresponding tool that makes it possible to write card programs in the concurrent thread model without losing compatibility with the existing Java Card API.

[29] Stephen Tse and Steve Zdancewic. Run-time Principals in Information-flow Type Systems. In IEEE 2004 Symposium on Security and Privacy (Oakland), pages 179-193. IEEE Computer Society Press, May 2004. [ PDF  PS ]
Information-flow type systems are a promising approach for enforcing strong end-to-end confidentiality and integrity policies. Such policies, however, are usually specified in term of static information-data is labeled high or low security at compile time. In practice, the confidentiality of data may depend on information available only while the system is running

This paper studies language support for run-time principals, a mechanism for specifying information-flow security policies that depend on which principals interact with the system. We establish the basic property of noninterference for programs written in such language, and use run-time principals for specifying run-time authority in downgrading mechanisms such as declassification.

In addition to allowing more expressive security policies, run-time principals enable the integration of language-based security mechanisms with other existing approaches such as Java stack inspection and public key infrastructures. We sketch an implementation of run-time principals via public keys such that principal delegation is verified by certificate chains.

[30] Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic. Enforcing Robust Declassification. In Proc. of 17th IEEE Computer Security Foundations Workshop (CSFW), pages 172-186, 2004. [ PDF ]
Noninterference requires that there is no information flow from sensitive to public data in a given system. However, many systems perform intentional release of sensitive information as part of their correct functioning and therefore violate noninterference. To control information flow while permitting intentional information release, some systems have a downgrading or declassification mechanism. A major danger of such a mechanism is that it may cause unintentional information release. This paper shows that a robustness property can be used to characterize programs in which declassification mechanisms cannot be exploited by attackers to release more information than intended. It describes a simple way to provably enforce this robustness property through a type-based compile-time program analysis. The paper also presents a generalization of robustness that supports upgrading (endorsing) data integrity.

[31] David Walker, Steve Zdancewic, and Jay Ligatti. A Theory of Aspects. In Proc. of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 127-139, Upsala, Sweden, August 2003. [ PDF  PS ]
This paper define the semantics of MinAML, an idealized aspect-oriented programming language, by giving a type-directed translation from its user-friendly external language to its compact, well-defined core language. We argue that our framework is an effective way to give semantics to aspect-oriented programming languages in general because the translation eliminates shallow syntactic differences between related constructs and permits definition of a clean, easy-to-understand, and easy-to-reason-about core language.

The core language extends the simply-typed lambda calculus with two central new abstractions: explicitly labeled program points and first-class advice. The labels serve both to trigger advice and to mark continuations that the advice may return to. These constructs are defined orthogonally to the other features of the language and we show that our abstractions can be used in both functional and object-oriented contexts. The labels are well-scoped and the language as a whole is well-typed. Consequently, programmers can use lexical scoping in the standard way to prevent aspects from interfering with local program invariants.

[32] Steve Zdancewic and Andrew C. Myers. Observational Determinism for Concurrent Program Security. In Proc. of 16th IEEE Computer Security Foundations Workshop (CSFW), pages 29-45, Asilomar, CA, July 2003. [ PDF  PS ]
Noninterference is a property of sequential programs that is useful for expressing security policies for data confidentiality and integrity. However, extending noninterference to concurrent programs has proved problematic. In this paper we present a relatively expressive secure concurrent language. This language, based on existing concurrent calculi, provides first-class channels, higher-order functions, and an unbounded number of threads. Well-typed programs obey a generalization of noninterference that ensures immunity to internal timing attacks and to attacks that exploit information about the thread scheduler. Elimination of these refinement attacks is possible because the enforced security property extends noninterference with observational determinism. Although the security property is strong, it also avoids some of the restrictiveness imposed on previous security-typed concurrent languages.

[33] Lantian Zheng, Stephen Chong, Steve Zdancewic, and Andrew C. Myers. Building Secure Distributed Systems Using Replication and Partitioning. In IEEE 2003 Symposium on Security and Privacy (Oakland), pages 236-250. IEEE Computer Society Press, 2003. [ PDF  PS ]
A challenging unsolved security problem is how to specify and enforce system-wide security policies; this problem is even more acute in distributed systems with mutual distrust. This paper describes a way to enforce policies for data confidentiality and integrity in such an environment. Programs annotated with security specifications are statically checked and then transformed by the compiler to run securely on a distributed system with untrusted hosts. The code and data of the computation are partitioned across the available hosts in accordance with the security specification. The key contribution is automatic replication of code and data to increase assurance of integrity-without harming confidentiality, and without placing undue trust in any host. The compiler automatically generates secure run-time protocols for communication among the replicated code partitions. Results are given from a prototype implementation applied to various distributed programs.

[34] Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. Untrusted Hosts and Confidentiality: Secure Program Partitioning. In Proc. 18th ACM Symp. on Operating System Principles (SOSP), volume 35(5) of Operating Systems Review, pages 1-14, Banff, Canada, October 2001. [ PDF  PS ]
This paper presents secure program partitioning, a language-based technique for protecting confidential data during computation in distributed systems containing mutually untrusted hosts. Confidentiality and integrity policies can be expressed by annotating programs with security types that constrain information flow; these programs can then be partitioned automatically to run securely on heterogeneously trusted hosts. The resulting communicating subprograms collectively implement the original program, yet the system as a whole satisfies the security requirements of participating principals without requiring a universally trusted host machine. The experience in applying this methodology and the performance of the resulting distributed code suggest that this is a promising way to obtain secure distributed computation.

[35] Steve Zdancewic and Andrew C. Myers. Robust Declassification. In Proc. of 14th IEEE Computer Security Foundations Workshop (CSFW), pages 15-23, Cape Breton, Canada, June 2001. [ PDF  PS ]
Security properties based on information flow, such as noninterference, provide strong guarantees that confidentiality is maintained. However, programs often need to leak some amount of confidential information in order to serve their intended purpose, and thus violate noninterference. Real systems that control information flow often include mechanisms for downgrading or declassifying information; however, declassification can easily result in the unexpected release of confidential information.

This paper introduces a formal model of information flow in systems that include intentional information leaks and shows how to characterize what information leaks. Further, we define a notion of robustness for systems that include information leaks introduced by declassification. Robust systems have the property that an attacker is unable to exploit declassification channels to obtain more confidential information than was intended to be released. We show that all systems satisfying a noninterference-like property are robust; for other systems, robustness involves a nontrivial interaction between confidentiality and integrity properties. We expect this model to provide new tools for the characterization of information flow properties in the presence of intentional information leaks.

[36] Steve Zdancewic and Andrew C. Myers. Secure Information Flow and CPS. In Proc. of the 10th European Symposium on Programming (ESOP), volume 2028 of Lecture Notes in Computer Science, pages 46-61, April 2001. [ PDF  PS ]
Security-typed languages enforce secrecy or integrity policies by type-checking. This paper investigates continuation-passing style as a means of proving that such languages enforce non-interference and as a first step towards understanding their compilation. We present a low-level, secure calculus with higher-order, imperative features. Our type system makes novel use of ordered linear continuations.

[37] Steve Zdancewic, Dan Grossman, and Greg Morrisett. Principals in Programming Languages: A Syntactic Proof Technique. In Proc. of the 4th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 197-207, Paris, France, September 1999. [ PDF  PS ]
Programs are often structured around the idea that different pieces of code comprise distinct principals, each with a view of its environment. Typical examples include the modules of a large program, a host and its clients, or a collection of interactive agents.

In this paper, we formalize this notion of principal in the programming language itself. The result is a language in which intuitive statements such as, “the client must call open to obtain a file handle”, can be phrased and proven formally.

We add principals to variants of the simply-typed lambda-calculus and show how we can track the code corresponding to each principal throughout evaluation. This multiagent calculus yields syntactic proofs of some type abstraction properties that traditionally require semantic arguments.

Workshop Papers
[1] Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic. Dependent Ineroperability. In The Sixth ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV), 2012. [ PDF ]
In this paper we study the problem of interoperability-combining constructs from two separate programming languages within one program-in the case where one of the two languages is dependently typed and the other is simply typed. We present a core calculus called SD, which combines dependently- and simply-typed sub-languages and supports user-defined (dependent) datatypes, among other standard features. SD has “boundary terms” that mediate the interaction between the two sub-languages. The operational semantics of SD demonstrates how the necessary dynamic checks, which must be done when passing a value from the simply-typed world to the dependently typed world, can be extracted from the dependent type constructors themselves, modulo user-defined functions for marshaling values across the boundary. We establish type-safety and other meta-theoretic properties of SD, and contrast this approach to others in the literature.

[2] Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. Lightweight linear types in System Fo. In ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI), pages 77-88, 2010. [ PDF ]
We present Fo, an extension of System F that uses kinds to distinguish between linear and unrestricted types, simplifying the use of linearity for general-purpose programming. We demonstrate through examples how Fo can elegantly express many useful protocols, and we prove that any protocol representable as a DFA can be encoded as an Fo type. We supply mechanized proofs of Fo's soundness and parametricity properties, along with a nonstandard operational semantics that formalizes common intuitions about linearity and aids in reasoning about protocols.

We compare Fo to other linear systems, noting that the simplicity of our kind-based approach leads to a more explicit account of what linearity is meant to capture, allowing otherwise-conflicting interpretations of linearity (in particular, restrictions on aliasing versus restrictions on resource usage) to coexist peacefully. We also discuss extensions to Fo aimed at making the core language more practical, including the additive fragment of linear logic, algebraic datatypes, and recursion.

[3] Michael J. May, Carl A. Gunter, Insup Lee, and Steve Zdancewic. Strong and Weak Policy Relations. In POLICY 2009, IEEE International Symposium on Policies for Distributed Systems and Networks, pages 33-36, 2009.
[4] Limin Jia and Steve Zdancewic. Encoding information flow in Aura. In Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security (PLAS), pages 17-29, 2009. [ PDF ]
Two of the main ways to protect security-sensitive resources in computer systems are to enforce access-control policies and information-flow policies. In this paper, we show how to enforce information-flow policies in AURA, which is a programming language for access control. When augmented with this mechanism for enforcing information-flow polices, AURA can further improve the security of reference monitors that implement access control.

We show how to encode security types and lattices of security labels using AURA's existing constructs for authorization logic. We prove a noninterference theorem for this encoding. We also investigate how to use expressive access-control policies specified in authorization logic as the policies for information declassification.

[5] Karl Mazurak and Steve Zdancewic. ABash: Finding Bugs in Bash Scripts. In ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), June 2007. [ PDF ]
This paper describes the design and implementation of ABash, a tool for statically analyzing programs written in the bash scripting language. Although it makes no formal guarantees against missed errors or spurious warnings (largely due to the highly dynamic nature of bash scripts), ABash is useful for detecting certain common program errors that may lead to security vulnerabilities. In experiments with 49 bash scripts taken from popular Internet repositories, ABash was able to identify 20 of them as containing bugs of varying severity while yielding only a reasonable number of spurious warnings on both these scripts and the generally bug-free initialization scripts of the Ubuntu Linux distribution. ABash works by performing abstract interpretation of a bash script via an abstract semantics that accounts for shell variable expansion. The analysis is also parameterized by a collection of signatures that describe external program interfaces (for Unix commands, etc.), yielding an easily configurable and extensible framework for finding bugs in bash scripts.

[6] Michael Hicks, Stephen Tse, Boniface Hicks, and Steve Zdancewic. Dynamic updating of information-flow policies. In Proc. of Foundations of Computer Security Workshop (FCS), 2005. [ PDF ]
Applications that manipulate sensitive information should ensure end-to-end security by satisfying two properties: sound execution and some form of noninterference. By the former, we mean the program should always perform actions in keeping with its current policy, and by the latter we mean that these actions should never cause high-security information to be visible to a low-security observer. Over the last decade, security-typed languages have been developed that exhibit these properties, increasingly improving so as to model important features of real programs.

No current security-typed language, however, permits general changes to security policies in use by running programs. This paper presents a simple information flow type system for that allows for dynamic security policy updates while ensuring sound execution and a relaxed form of noninterference we term noninterference between updates. We see this work as an important step toward using language-based techniques to ensure end-to-end security for realistic applications.

[7] Peng Li and Steve Zdancewic. Unifying Confidentiality and Integrity in Downgrading Policies. In Proc. of Foundations of Computer Security Workshop (FCS), 2005. [ PDF ]
Confidentiality and integrity are often treated as dual properties in formal models of information-flow control, access control and many other areas in computer security. However, in contrast to confidentiality policies, integrity policies are less formally studied in the information-flow control literature. One important reason is that traditional noninterference-based information-flow control approaches give very weak integrity guarantees for untrusted code. Integrity and confidentiality policies are also different with respect to implicit information channels.

This paper studies integrity downgrading policies in information-flow control and compares them with their confidentiality counterparts. We examine the drawbacks of integrity policies based on noninterference formalizations and study the integrity policies in the framework of downgrading policies and program equivalences. We give semantic interpretations for traditional security levels for integrity, namely, tainted and untainted, and explain the interesting relations between confidentiality and integrity in this framework.

[8] Peng Li, Yun Mao, and Steve Zdancewic. Information Integrity Policies. In Proceedings of the Workshop on Formal Aspects in Security & Trust (FAST), September 2003. [ PDF  PS ]
Information integrity policies are traditionally enforced by access control mechanisms that prevent unauthorized users from modifying data. However, access control does not provide end-to-end assurance of integrity. For that reason, integrity guarantees in the form of noninterference assertions have been proposed. Despite the appeals of such information-flow based approaches to integrity, that solution is also unsatisfactory because it leads to a weaker notion of integrity than needed in practice.

This paper attempts to clarify integrity policies by comparing and contrasting access control vs. information flow, integrity vs. confidentiality policies, and integrity vs. availability policies. The paper also examines data invariants as a way to strengthen integrity. The result is a better classification of information-integrity policies.

[9] Usa Sammapun, Raman Sharykin, Margaret Delap, Myong Kim, and Steve Zdancewic. Formalizing Java-MaC. In Proceedings of the Third Runtime Verification Workshop, pages 171-190. Electronic Notes in Theoretical Computer Science, July 2003. [ PDF  PS ]
The Java-MaC framework is a run-time verification system for Java programs that can be used to dynamically test and enforce safety policies. This paper presents a formal model of the Java-MaC safety properties in terms of an operational semantics for Middleweight Java, a realistic subset of full Java. This model is intended to be used as a framework for studying the correctness of Java-MaC program instrumentation, optimizations, and future experimentation with run-time monitor expressiveness. As a preliminary demonstration of this model's applicability for these tasks, the paper sketches a correctness result for a simple program instrumentation scheme.

[10] Michael Greenwald, Carl A. Gunter, Björn Knutsson, Andre Scedrov, Jonathan M. Smith, and Steve Zdancewic. Computer Security is Not a Science (but it should be). In Proceedings of the Large-Scale Network Security Workshop, March 2003. [ PDF  PS ]
[11] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A Realistic Typed Assembly Language. In 2nd ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25-35, 1999. [ PDF  PS ]
The goal of typed assembly language (TAL) is to provide a low-level, statically typed target language that is better suited than Java bytecodes for supporting a wide variety of source languages and a number of important optimizations. In previous work, we formalized idealized versions of TAL and proved important safety properties about them. In this paper, we present our progress in defining and implementing a realistic typed assembly language called TALx86. The TALx86 instructions comprise a relatively complete fragment of the Intel IA32 (32-bit 80x86 flat model) assembly language and are thus executable on processors such as the Intel Pentium. The type system for the language incorporates a number of advanced features necessary for safely compiling large programs to good code.

To motivate the design of the type system, we demonstrate how various high-level language features are compiled to TALx86. For this purpose, we present a type-safe C-like language called Popcorn.

Edited Volumes
[1] Pierpaolo Degano, Ralf Küsters, Luca Viganò, and Steve Zdancewic, editors. Joint workshop on foundations of computer security and automated reasoning for security protocol analysis (FCS-ARSPA '06), volume 206 of Information and Computation. Elsevier, 2008.
[2] Vugranam C. Shreedhar and Steve Zdancewic, editors. Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security (PLAS). ACM, 2006.
Technical Reports, Work in Progress, and Unpublished Papers
[1] Jennifer Paykin and Steve Zdancewic. A Linear/Producer/Consumer model of Classical Linear Logic. Technical report, University of Pennsylvania, 2014. [ PDF ]
This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions that reflect the linear/producer/consumer structure. The paper's metatheoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into the category theory. The work also presents several concrete instances of the LPC model, including one based on finite vector spaces.

[2] Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M.K. Martin, and Steve Zdancewic. Ironclad C++: A library-Augmented Type-Safe Subset of C++. Technical Report MS-CIS-13-05, University of Pennsylvania, MAR 2013. [ PDF ]
[3] Brian Aydemir, Stephanie Weirich, and Steve Zdancewic. Abstracting Syntax. (15 pages), 2008.
[4] Stephen Tse and Steve Zdancewic. Concise Concrete Syntax. Technical Report MS-CIS-08-11, University of Pennsylvania, 2008. [ PDF ]
[5] Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. AURA:Preliminary Technical Results. Technical Report MS-CIS-08-10, University of Pennsylvania, 2008. [ PDF ]
[6] Jeffrey C. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic. Evidence-based Audit, Technical Appendix. Technical Report MS-CIS-08-09, University of Pennsylvania, 2008. [ PDF ]
[7] Stephen Tse and Steve Zdancewic. Translating Dependency into Parametricity. (33 pages) Accepted to Journal of Functional Programming, pending revisions, 2006.
[8] Stephen Tse and Steve Zdancewic. Designing a Security-typed Language with Certificate-based Declassification. Technical Report MIS-CIS-04-16, University of Pennsylvania, 2004. [ PDF ]
This paper presents the design of a programming language that supports information-flow security policies and certificate-based declassification.

The language uses monadic information-flow annotations in the style of Abadi et al.'s dependency core calculus, and has an effects system and fixpoints. The type system conflates security concepts such as labels, principals, and privileges with abstract types, allowing a uniform treatment of lattice structures throughout the language. Myers' and Liskov's decentralized label model is encoded using type constructors that describe confidentiality and integrity policies, and label refinements and principal groups follow naturally from intersection and union types. Singleton types, combined with bounded universal and existential quantifications, connect the type system with public-key infrastructures whose digital certificates provide authorization for privileged operations such as declassification. These features allow specification of security policies in term of dynamic entities such as run-time user identities and file access permissions.

Besides showing that the language is sound, we present a security theorem that generalizes standard noninterference to account for information flows introduced by declassification. Although this result gives only a coarse approximation to the information potentially leaked, it captures our intuitions about certificate-based declassification.

[9] Stephen Tse and Steve Zdancewic. Translating Dependency into Parametricity. Technical Report MIS-CIS-04-01, University of Pennsylvania, 2004. [ PDF ]
The dependency core calculus (DCC) was introduced by Abadi et al. as a unifying formal framework in which to study a variety of important program analyses including binding-time, information-flow, slicing, and function call tracking. The novel feature of DCC is a lattice of monads and a nonstandard typing rule for their associated bind operations. Intuitively, the lattice structure describes which computations in a program may depend on each other. Abadi et al. prove a noninterference result that establishes the correctness of DCC's type system, and they use that result to show that type systems for the above-mentioned analyses are correct. In this paper, we study the relationship between DCC and the Girard-Reynolds polymorphic lambda calculus (System F). In particular, we show how to encode the recursion-free fragment of DCC into F via a type-directed translation. The main theorem we present uses this translation to derive the noninterference result for DCC from the standard parametricity theorem of System F. In addition to providing insight into DCC's type system, the hope is that the translation presented here may yield implementation strategies for non-standard type systems (e.g. for information flow security) in languages that have parametric polymorphism.

[10] Stephen Tse and Steve Zdancewic. Run-time Principals in Information-flow Type Systems. Technical Report MS-CIS-03-39, University of Pennsylvania, 2003. The conference version appears in IEEE Security and Privacy 2004. [ PDF  PS ]
Information-flow type systems are a promising approach for enforcing strong end-to-end confidentiality and integrity policies. Such policies, however, are usually specified in term of static information-data is labeled high or low security at compile time. In practice, the confidentiality of data may depend on information available only while the system is running

This paper studies language support for run-time principals, a mechanism for specifying information-flow security policies that depend on which principals interact with the system. We establish the basic property of noninterference for programs written in such language, and use run-time principals for specifying run-time authority in downgrading mechanisms such as declassification.

In addition to allowing more expressive security policies, run-time principals enable the integration of language-based security mechanisms with other existing approaches such as Java stack inspection and public key infrastructures. We sketch an implementation of run-time principals via public keys such that principal delegation is verified by certificate chains.

[11] Stephan A. Zdancewic. Programming Languages for Information Security. PhD thesis, Cornell University, August 2002. [ PDF  PS ]
Our society's widespread dependence on networked information systems for everything from personal finance to military communications makes it essential to improve the security of software. Standard security mechanisms such as access control and encryption are essential components for protecting information, but they do not provide end-to-end guarantees. Programming-languages research has demonstrated that security concerns can be addressed by using both program analysis and program rewriting as powerful and flexible enforcement mechanisms.

This thesis investigates security-typed programming languages, which use static typing to enforce information-flow security policies. These languages allow the programmer to specify confidentiality and integrity constraints on the data used in a program; the compiler verifies that the program satisfies the constraints.

Previous theoretical security-typed languages research has focused on simple models of computation and unrealistically idealized security policies. The existing practical security-typed languages have not been proved to guarantee security. This thesis addresses these limitations in several ways.

First, it establishes noninterference, a basic information-flow policy, for languages richer than those previously considered. The languages studied here include recursive, higher-order functions, structured state, and concurrency. These results narrow the gap between the theory and the practice of security-typed languages.

Next, this thesis considers more practical security policies. Noninterference is often too restrictive for real-world programming. To compensate, a restricted form of declassification is introduced, allowing programmers to specify a richer set of information-flow policies. Previous work on information-flow security also assumed that all computation occurs on equally trusted machines. To overcome this unrealistic premise, additional security constraints for systems distributed among heterogeneously trusted hosts are considered.

Finally, this thesis describes Jif/split, a prototype implementation of secure program partitioning, in which a program can automatically be partitioned to run securely on heterogeneously trusted hosts. The resulting communicating subprograms collectively implement the original program, yet the system as a whole satisfies the security requirements without needing a universally trusted machine. The theoretical results developed earlier in the thesis justify Jif/split's run-time enforcement mechanisms.

[12] Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. Secure Program Partitioning. Technical Report 2001-1846, Computer Science Dept., Cornell University, 2001. [ PDF  PS ]
This paper presents secure program partitioning, a language-based technique for protecting confidential data during computation in distributed systems containing mutually untrusted hosts. Confidentiality and integrity policies can be expressed by annotating programs with security types that constrain information flow; these programs can then be partitioned automatically to run securely on heterogeneously trusted hosts. The resulting communicating subprograms collectively implement the original program, yet the system as a whole satisfies the security requirements of participating principals without requiring a universally trusted host machine. The experience in applying this methodology and the performance of the resulting distributed code suggest that this is a promising way to obtain secure distributed computation.

This Technical Report is an expanded version of the published paper “Untrusted Hosts and Confidentiality: Secure Program Partitioning”. The main difference between the two is Appendix A, which contains a correctness proof for the control-transfer protocols described in Section 5.

[13] Steve Zdancewic and Andrew C. Myers. Confidentiality and Integrity with Untrusted Hosts. Technical Report 2000-1810, Computer Science Dept., Cornell University, 2000. [ PDF  PS ]
Several security-typed languages have recently been proposed to enforce security properties such as confidentiality or integrity by type checking. We propose a new security-typed language, Spl@, that addresses two important limitations of previous approaches.

First, existing languages assume that the underlying execution platform is trusted; this assumption does not scale to distributed computation in which a variety of differently trusted hosts are available to execute programs. Our new approach, secure program partitioning, translates programs written assuming complete trust in a single executing host into programs that execute using a collection of variously trusted hosts to perform computation. As the trust configuration of a distributed system evolves, this translation can be performed as necessary for security.

Second, many common program transformations do not work in existing security-typed languages; although they produce equivalent programs, these programs are rejected because of apparent information flows. Spl@ uses a novel mechanism based on ordered linear continuations to permit a richer class of program transformations, including secure program partitioning.

[14] Steve Zdancewic and Dan Grossman. Principals in Programming Languages: Technical Results. Technical Report TR99-1752, Computer Science Dept., Cornell University, June 1999. [ PDF  PS ]
This is the companion technical report for “Principals in Programming Languages: A Syntactic Proof Technique.” See that document for a more readable version of these results.

In this paper, we describe two variants of the simply typed lambda-calculus extended with a notion of principal. The results are languages in which intuitive statements like “the client must call open to obtain a file handle” can be phrased and proven formally.

The first language is a two-agent calculus with references and recursive types, while the second language explores the possibility of multiple agents with varying amounts of type information. We use these calculi to give syntactic proofs of some type abstraction results that traditionally require semantic arguments.

Copyright Information
The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Parts of this page were generated by bibtex2html Last modified: Thu May 8 19:48:11 EDT 2014