This is a collection of technical reports from the Cornell's Computing and Information Science (CIS) Department from the time period of 2003-present. These reports are part of the NCSTRL collection of Computer Science Technical Reports.

For reports prior to 2003, see the Computer Science Technical Reports Collection.

Recent Submissions

  • Full-Processor Timing Channel Protection with Applications to Secure Hardware Compartments 

    Ferraiuolo, Andrew; Wang, Yao; Xu, Rui; Zhang, Danfeng; Myers, Andrew; Suh, Edward (2015)
    This paper presents timing compartments, a hardware architecture abstraction that eliminates microarchitectural timing channels between groups of processes of VMs running on shared hardware. When coupled ...
  • Regular Expressions with Dynamic Name Binding 

    Kozen, Dexter; Milius, Stefan; Schröder, Lutz; Wißmann, Thorsten (2015-10-18)
    Nominal Kleene algebra (NKA) is a formalism to specify trace languages with name generation; it extends standard regular expressions with a name binding construct. NKA has been proved complete over a natural nominal language ...
  • Election Verifiability: Cryptographic Definitions and an Analysis of Helios and JCJ 

    Smyth, Ben; Frink, Steven; Clarkson, Michael R. (2015-08-06)
    Definitions of election verifiability in the computational model of cryptography are proposed. The definitions formalize notions of voters verifying their own votes, auditors verifying the tally of votes, and auditors ...
  • Probabilistic NetKAT 

    Foster, Nate; Kozen, Dexter; Mamouras, Konstantinos; Reitblatt, Mark; Silva, Alexandra (2015-07)
    This paper develops a new language for programming software-defined networks based on a probabilistic semantics. We extend the NetKAT language with new primitives for expressing probabilistic behaviors and enrich the ...
  • Genus: Making Generics Object-Oriented, Expressive, and Lightweight 

    Zhang, Yizhou; Loring, Matthew C.; Salvaneschi, Guido; Liskov, Barbara; Myers, Andrew C. (2015-04-15)
    The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanism that adds expressive power and strengthens ...
  • Computational Election Verifiability: Definitions and an Analysis of Helios and JCJ 

    Smyth, Ben; Frink, Steven; Clarkson, Michael R. (2015-04-13)
    Definitions of election verifiability in the computational model of cryptography are proposed. The definitions formalize notions of voters verifying their own votes, auditors verifying the tally of votes, and auditors ...
  • Diagnosing Type Errors with Class 

    Zhang, Danfeng; Myers, Andrew C.; Vytiniotis, Dimitrios; Jones, Simon Peyton (2015-04-12)
    Type inference engines often give terrible error messages, and the more sophisticated the type system the worse the problem. We show that even with highly expressive type system implemented by the Glasgow Haskell Compiler ...
  • Nominal Kleene Coalgebra 

    Kozen, Dexter; Mamouras, Konstantinos; Petrisan, Daniela; Silva, Alexandra (2015-02-18)
    We develop the coalgebraic theory of nominal Kleene algebra, including an alternative language-theoretic semantics, a nominal extension of the Brzozowski derivative, and a bisimulation-based decision procedure for the ...
  • Completeness and Incompleteness in Nominal Kleene Algebra 

    Kozen, Dexter; Mamouras, Konstantinos; Silva, Alexandra (2014-11-14)
    Gabbay and Ciancia (2011) presented a nominal extension of Kleene algebra as a framework for trace semantics with dynamic allocation of resources, along with a semantics consisting of nominal languages. They also provided ...
  • Merlin: A Language for Provisioning Network Resources 

    Soulé, Robert; Basu, Shrutarshi; Marandi, Parisa Jalili; Pedone, Fernando; Kleinberg, Robert; Sirer, Emin Gün; Foster, Nate (2014-06-25)
    This paper presents Merlin, a new framework for managing resources in software-defined networks. With Merlin, administrators express high-level policies using programs in a declarative language. The language includes logical ...
  • A Metrized Duality Theorem for Markov Processes 

    Kozen, Dexter; Mardare, Radu; Panangaden, Prakash (2014-05-21)
    We extend our previous duality theorem for Markov processes by equipping the processes with a pseudometric and the algebras with a notion of metric diameter. We are able to show that the isomorphisms of our previous duality ...
  • Fine-Grained User Privacy from Avenance Tags 

    Birrell, Eleanor; Schneider, Fred B. (2014-04-20)
    In the Internet, users interact with service providers; these interactions exchange information that might be considered private by the user. Existing schemes for expressing and enforcing user privacy on the Internet---notably ...
  • A Hardware Design Language for Efficient Control of Timing Channels 

    Zhang, Danfeng; Wang, Yao; Suh, G. Edward; Myers, Andrew C. (2014-04-10)
    Timing channels pose a real security risk, but methods are lacking for building systems without timing leaks. One reason is that low-level hardware features create timing channels; for example, caches enable probing attacks. ...
  • A Coalgebraic Decision Procedure for NetKAT 

    Foster, Nate; Kozen, Dexter; Milano, Matthew; Silva, Alexandra; Thompson, Laure (2014-03-26)
    Program equivalence is a fundamental problem that has practical applications across a variety of areas of computing including compilation, optimization, software synthesis, formal verification, and many others. Equivalence ...
  • Kleene Algebra with Equations 

    Kozen, Dexter; Mamouras, Konstantinos (2014-02-27)
    We identify sufficient conditions for the construction of free language models for systems of Kleene algebra with additional equations. The construction applies to a broad class of extensions of KA and provides a uniform ...
  • A Language for Securely Referencing Persistent Information in a Federated System 

    Liu, Jed; Myers, Andrew C. (2014-01-17)
    Referential integrity, which guarantees that named resources can be accessed when referenced, is an important property for reliability and security. In distributed systems, however, the attempt to provide referential ...
  • KAT + B! 

    Grathwohl, Niels Bjørn Bugge; Kozen, Dexter; Mamouras, Konstantinos (2014-01-08)
    It is known that certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests (KAT). In this paper we show how to axiomatically extend KAT with ...
  • NetKAT: Semantic Foundations for Networks 

    Anderson, Carolyn Jane; Foster, Nate; Guha, Arjun; Jeannin, Jean-Baptiste; Kozen, Dexter; Schlesinger, Cole; Walker, David (2013-10-11)
    Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network ...
  • Toward General Diagnosis of Static Errors: Technical Report 

    Zhang, Danfeng; Myers, Andrew (2013-08-22)
    We introduce a general way to locate program errors that are detected by type systems and other program analyses. The program analysis is expressed in a constraint language in which program errors manifest as unsatisfiable ...
  • Infinitary Axiomatization of the Equational Theory of Context-Free Languages 

    Grathwohl, Niels Bjørn Bugge; Henglein, Fritz; Kozen, Dexter (2013-07-01)
    We give a natural complete infinitary axiomatization of the equational theory of the context-free languages, answering a question of Leiss (1992).

View more


RSS Feeds