Computing and Information Science Technical Reportshttp://hdl.handle.net/1813/56022017-06-19T13:23:20Z2017-06-19T13:23:20ZPushing Bytes: Cloud-Scale Data Replication with RDMCBehrens, JonathanJha, SagarTremel, EdwardBirman, Kenhttp://hdl.handle.net/1813/514892017-06-17T07:00:56Z2017-06-01T00:00:00ZPushing Bytes: Cloud-Scale Data Replication with RDMC
Behrens, Jonathan; Jha, Sagar; Tremel, Edward; Birman, Ken
Data center infrastructures frequently replicate objects to create backups or to copy executables and input files to compute nodes. This task occurs under time pressure: data is at risk of loss until replicated for fault-tolerance, and in the case of parallel processing systems like Spark, useful computation can't start until the nodes all have a copy of the executable images. Cloud elasticity creates a similar need to rapidly copy executables and their inputs. To address these needs, we introduce RDMC: a fast reliable data replication protocol that implements multicast as a pattern of RDMA unicast operations, which maximizes concurrency while minimizing unnecessary transfers. RDMC can be used in any setting that has RDMA or a software RDMA emulation. Our focus is on use of replication as an element of the data center infrastructure. We evaluate overheads for the hardware-supported case using microbenchmarks and heavy-load experiments, and also describe preliminary experiments using a technique that offloads the entire data transfer pattern into the NICs, further reducing latency while freeing server resources for other tasks.
2017-06-01T00:00:00ZShoal: A Lossless Network for High-density and Disaggregated RacksShrivastav, VishalValadarsky, AsafBallani, HiteshCosta, PaoloLee, Ki SuhWang, HanAgarwal, RachitWeatherspoon, Hakimhttp://hdl.handle.net/1813/496472017-05-08T12:58:36Z2017-04-30T00:00:00ZShoal: A Lossless Network for High-density and Disaggregated Racks
Shrivastav, Vishal; Valadarsky, Asaf; Ballani, Hitesh; Costa, Paolo; Lee, Ki Suh; Wang, Han; Agarwal, Rachit; Weatherspoon, Hakim
Rack-scale computers comprise hundreds of micro-servers connected to internal storage and memory through an internal network. However, their density and disaggregated nature pose a problem for existing packet-switched networks: they are too costly, draw too much power, and the network latency is too high for converged traffic (comprising IP, storage, and memory traffic). We propose Shoal, a rack-scale network that tightly integrates a circuit-switched physical fabric with the nodes’ network stack to efficiently support converged traffic. Shoal’s fabric comprises circuit switches with no buffers, no arbitration, and no packet inspection mechanism. Micro-servers transmit according to a static schedule such that there is no in-network contention. Shoal’s congestion control leverages the physical fabric to achieve fairness, losslessness, and both bounded worst-case throughput and queuing. We use an FPGA-based prototype and simulations to illustrate Shoal’s mechanisms are practical and achieve low latency within the rack at low cost and power.
2017-04-30T00:00:00ZFull-Processor Timing Channel Protection with Applications to Secure Hardware CompartmentsFerraiuolo, AndrewWang, YaoXu, RuiZhang, DanfengMyers, AndrewSuh, Edwardhttp://hdl.handle.net/1813/412182017-04-25T14:34:50Z2017-04-25T00:00:00ZFull-Processor Timing Channel Protection with Applications to Secure Hardware Compartments
Ferraiuolo, Andrew; Wang, Yao; Xu, Rui; Zhang, Danfeng; Myers, Andrew; Suh, Edward
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 with conventional access controls, timing compartments provide
strong isolation comparable to running software entities on separate
machines. Timing compartments use microarchitecture mechanisms to enforce
timing sensitive noninterference, which we prove formally through
information flow analysis of an RTL implementation. In the process of
systematically removing timing interference, we identify and remove new
sources of timing channels, including cache coherence mechanisms and module
interfaces, and introduce new performance optimizations. We also
demonstrate how timing compartments may be extended to support a
hardware-only TCB which ensures security even when the system is managed
by an untrusted OS or hypervisor. The overheads of timing compartments are
low; compared to a comparable insecure baseline, executing two timing
compartments reduces system throughput by less than 7% on average and by
less than 2% for compute-bound workloads.
2017-04-25T00:00:00ZUnrestricted Stone Duality for Markov ProcessesFurber, RobertKozen, DexterLarsen, KimMardare, RaduPanangaden, Prakashhttp://hdl.handle.net/1813/463022017-02-24T08:01:24Z2017-02-23T00:00:00ZUnrestricted Stone Duality for Markov Processes
Furber, Robert; Kozen, Dexter; Larsen, Kim; Mardare, Radu; Panangaden, Prakash
Stone duality relates logic, in the form of Boolean algebra, to spaces. Stone-type dualities abound in computer science and have been of great use in understanding the relationship between computational models and the languages used to reason about them. Recent work on probabilistic processes has established a Stone-type duality for a restricted class of Markov processes. The dual category was a new notion--Aumann algebras--which are Boolean algebras equipped with countable family of modalities indexed by rational probabilities. In this article we consider an alternative definition of Aumann algebra that leads to dual adjunction for Markov processes that is a duality for many measurable spaces occurring in practice. This extends a duality for measurable spaces due to Sikorski. In particular, we do not require that the probabilistic modalities preserve a distinguished base of clopen sets, nor that morphisms of Markov processes do so. The extra generality allows us to give a perspicuous definition of event bisimulation on Aumann algebras.
2017-02-23T00:00:00ZElection Verifiability: Cryptographic Definitions and an Analysis of Helios and JCJSmyth, BenFrink, StevenClarkson, Michael R.http://hdl.handle.net/1813/405752017-02-17T08:01:16Z2017-02-13T00:00:00ZElection Verifiability: Cryptographic Definitions and an Analysis of Helios and JCJ
Smyth, Ben; Frink, Steven; Clarkson, Michael R.
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 verifying that only eligible voters vote. The Helios (Adida et
al., 2009) and JCJ (Juels et al., 2010) election schemes are analyzed
using these definitions. Helios 4.0 satisfies the definitions, but
Helios 2.0 does not because of previously known attacks. JCJ does not
satisfy the definitions because of a trust assumption it makes, but it
does satisfy a weakened definition. Two previous definitions of
verifiability (Juels et al., 2010; Cortier et al., 2014) are shown to
permit election schemes vulnerable to attacks, whereas the new
definitions prohibit those schemes.
2017-02-13T00:00:00ZMixing Consistency in Geodistributed Transactions: Technical ReportMilano, Matthew P.Myers, Andrew C.http://hdl.handle.net/1813/447102016-10-08T05:01:03Z2016-10-07T00:00:00ZMixing Consistency in Geodistributed Transactions: Technical Report
Milano, Matthew P.; Myers, Andrew C.
Weakly consistent data stores have become popular because they enable highly available, scalable distributed applications. However, some data needs strong consistency. For applications that mix accesses to strongly and weakly consistent data, programmers must currently choose between bad performance and possible data corruption. We instead introduce a safe mixed-consistency programming model in which programmers choose the consistency level on a per-object basis. Further, they can use atomic, isolated transactions to access both strongly consistent (e.g., linearizable) data and weakly consistent (e.g., causally consistent) data within the same transaction. Compile-time checking ensures that mixing consistency levels is safe: the guarantees of each object's consistency level are enforced. Programmers avoid being locked into one consistency level; they can make an application-specific tradeoff between performance and consistency. We have implemented this programming model as part of a new system called MyriaStore. MyriaStore demonstrates that safe mixed consistency can be implemented on top of off-the-shelf data stores with their own native, distinct consistency guarantees. Our performance measurements demonstrate that significant performance improvements can be obtained for geodistributed applications that need strong consistency for some critical operations but that also need the high performance and low latency possible with causally consistent data.
2016-10-07T00:00:00ZSafe Serializable Secure Scheduling: Transactions and the Trade-Off Between Security and Consistency (Technical Report)Sheff, IsaacMagrino, TomLiu, JedMyers, Andrew C.van Renesse, Robberthttp://hdl.handle.net/1813/445812016-08-17T05:01:27Z2016-08-16T00:00:00ZSafe Serializable Secure Scheduling: Transactions and the Trade-Off Between Security and Consistency (Technical Report)
Sheff, Isaac; Magrino, Tom; Liu, Jed; Myers, Andrew C.; van Renesse, Robbert
Modern applications often operate on data in multiple administrative domains. In this federated setting, participants may not fully trust each other. These distributed applications use transactions as a core mechanism for ensuring reliability and consistency with persistent data. However, the coordination mechanisms needed for transactions can both leak confidential information and allow unauthorized influence.
By implementing a simple attack, we show these side channels can be exploited. However, our focus is on preventing such attacks. We explore secure scheduling of atomic, serializable transactions in a federated setting. While we prove that no protocol can guarantee security and liveness in all settings, we establish conditions for sets of transactions that can safely complete under secure scheduling. Based on these conditions, we introduce staged commit, a secure scheduling protocol for federated transactions. This protocol avoids insecure information channels by dividing transactions into distinct stages. We implement a compiler that statically checks code to ensure it meets our conditions, and a system that schedules these transactions using the staged commit protocol. Experiments on this implementation demonstrate that realistic federated transactions can be scheduled securely, atomically, and efficiently.
2016-08-16T00:00:00ZAccepting Blame: Expressive Checked ExceptionsZhang, YizhouSalvaneschi, GuidoBeightol, QuinnLiskov, BarbaraMyers, Andrew C.http://hdl.handle.net/1813/437842016-04-19T05:02:12Z2016-04-01T00:00:00ZAccepting Blame: Expressive Checked Exceptions
Zhang, Yizhou; Salvaneschi, Guido; Beightol, Quinn; Liskov, Barbara; Myers, Andrew C.
Unhandled exceptions crash programs, so a compile-time check that exceptions are handled should in principle make software more reliable. But designers of some recent languages have argued that the benefits of statically checked exceptions are not worth the costs. We introduce a new statically checked exception mechanism that addresses the problems with existing checked-exception mechanisms. In particular, it interacts well with higher-order functions and other design patterns. The key insight is that whether an exception should be treated as a “checked” exception is not a property of its type but rather of the context in which the exception propagates. Statically checked exceptions can “tunnel” through code that is oblivious to their presence, but the type system nevertheless checks that these exceptions are handled. Further, exceptions can be tunneled without being accidentally caught, by expanding the space of exception identifiers to identify the exception-handling context. The resulting mechanism is expressive, syntactically light, and can be implemented efficiently. We demonstrate the expressiveness of the mechanism using significant codebases and evaluate its performance. We have implemented this new exception mechanism as part of the new Genus programming language, but the mechanism could equally well be applied to other programming languages.
2016-04-01T00:00:00ZGenus: Making Generics Object-Oriented, Expressive, and LightweightZhang, YizhouLoring, Matthew C.Salvaneschi, GuidoLiskov, BarbaraMyers, Andrew C.http://hdl.handle.net/1813/399102016-04-19T05:01:56Z2015-06-01T00:00:00ZGenus: Making Generics Object-Oriented, Expressive, and Lightweight
Zhang, Yizhou; Loring, Matthew C.; Salvaneschi, Guido; Liskov, Barbara; Myers, Andrew C.
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 static checking, while remaining lightweight and simple in common use cases. Like type classes and concepts, the mechanism allows existing types to model type constraints retroactively. For expressive power, we expose models as named constructs that can be defined and selected explicitly to witness constraints; in common uses of genericity, however, types implicitly witness constraints without additional programmer effort. Models are integrated into the object-oriented style, with features like model generics, model-dependent types, model enrichment, model multimethods, constraint entailment, model inheritance, and existential quantification further extending expressive power in an object-oriented setting. We introduce the new genericity features and show that common generic programming idioms, including current generic libraries, can be expressed more precisely and concisely. The static semantics of the mechanism and a proof of a key decidability property are provided.
Content file updated at author's request on 2015-04-30.
2015-06-01T00:00:00ZKolmogorov Extension, Martingale Convergence, and Compositionality of ProcessesKozen, Dexterhttp://hdl.handle.net/1813/415172016-01-01T06:00:48Z2015-12-30T00:00:00ZKolmogorov Extension, Martingale Convergence, and Compositionality of Processes
Kozen, Dexter
We show that the Kolmogorov extension theorem and the Doob martingale convergence theorem are two aspects of a common generalization, namely a colimit-like construction in a category of Radon spaces and reversible Markov kernels. The construction provides a compositional denotational semantics for standard iteration operators in programming languages, e.g. Kleene star or while loops, as a limit of finite approximants, even in the absence of a natural partial order.
2015-12-30T00:00:00ZRegular Expressions with Dynamic Name BindingKozen, DexterMilius, StefanSchröder, LutzWißmann, Thorstenhttp://hdl.handle.net/1813/411882016-03-04T06:02:23Z2015-10-18T00:00:00ZRegular Expressions with Dynamic Name Binding
Kozen, Dexter; Milius, Stefan; Schröder, Lutz; Wißmann, Thorsten
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 model. Moreover, it has been shown that NKA expressions can be translated into a species of nondeterministic nominal automata, thus providing one half of a Kleene theorem. The other half is known to fail, i.e. there are nominal languages that can be accepted by a nominal automaton but are not definable in NKA. In the present work, we introduce a calculus of regular expressions with dynamic name binding. It satisfies the full Kleene theorem, i.e. it is equivalent to a natural species of nominal automata, and thus strictly more expressive than NKA. We show that containment checking in our calculus is decidable in EXPSPACE, and in fact has polynomial fixed-parameter space complexity. The known EXPSPACE bound for containment of NKA expressions follows.
Content file updated at author's request on 2016-03-03.
2015-10-18T00:00:00ZProbabilistic NetKATFoster, NateKozen, DexterMamouras, KonstantinosReitblatt, MarkSilva, Alexandrahttp://hdl.handle.net/1813/403352015-07-14T05:02:27Z2015-07-01T00:00:00ZProbabilistic NetKAT
Foster, Nate; Kozen, Dexter; Mamouras, Konstantinos; Reitblatt, Mark; Silva, Alexandra
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 semantics from one based on deterministic functions to one based on measures and measurable functions on sets of packet histories. We establish fundamental properties of the semantics, prove that it is a conservative extension of the deterministic semantics, and show that it satisfies a number of natural equations. We present case studies that show how the language can be used to model a diverse collection of scenarios drawn from real-world networks.
2015-07-01T00:00:00ZComputational Election Verifiability: Definitions and an Analysis of Helios and JCJSmyth, BenFrink, StevenClarkson, Michael R.http://hdl.handle.net/1813/399082015-07-08T11:53:24Z2015-04-13T00:00:00ZComputational Election Verifiability: Definitions and an Analysis of Helios and JCJ
Smyth, Ben; Frink, Steven; Clarkson, Michael R.
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 verifying that only eligible voters vote. The Helios (Adida et
al., 2009) and JCJ (Juels et al., 2010) election schemes are shown to
satisfy these definitions. Two previous definitions (Juels et al., 2010;
Cortier et al., 2014) are shown to permit election schemes vulnerable to
attacks, whereas the new definitions prohibit those schemes.
Content file updated at author's request on 2015-05-01.
2015-04-13T00:00:00ZDiagnosing Type Errors with ClassZhang, DanfengMyers, Andrew C.Vytiniotis, DimitriosJones, Simon Peytonhttp://hdl.handle.net/1813/399072015-07-09T00:38:15Z2015-04-12T00:00:00ZDiagnosing Type Errors with Class
Zhang, Danfeng; Myers, Andrew C.; Vytiniotis, Dimitrios; Jones, Simon Peyton
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 (GHC)--including type classes, GADTs, and type families—it is possible to identify the most likely source of the type error, rather than the first source that the inference engine trips over. To determine which are the likely error sources, we apply a simple Bayesian model to a graph representation of the typing constraints; the satisfiability or unsatisfiability of paths within the graph provides evidence for or against possible explanations. While we build on prior work on error diagnosis for simpler type systems, inference in the richer type system of Haskell requires extending the graph with new nodes. The augmentation of the graph creates challenges both for Bayesian reasoning and for ensuring termination. Using a large corpus of Haskell programs, we show that this error localization technique is practical and significantly improves accuracy over the state of the art.
2015-04-12T00:00:00ZNominal Kleene CoalgebraKozen, DexterMamouras, KonstantinosPetrisan, DanielaSilva, Alexandrahttp://hdl.handle.net/1813/391082015-07-08T08:10:40Z2015-02-18T00:00:00ZNominal Kleene Coalgebra
Kozen, Dexter; Mamouras, Konstantinos; Petrisan, Daniela; Silva, Alexandra
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 equational theory.
2015-02-18T00:00:00ZCompleteness and Incompleteness in Nominal Kleene AlgebraKozen, DexterMamouras, KonstantinosSilva, Alexandrahttp://hdl.handle.net/1813/381432015-07-08T11:19:45Z2014-11-14T00:00:00ZCompleteness and Incompleteness in Nominal Kleene Algebra
Kozen, Dexter; Mamouras, Konstantinos; Silva, Alexandra
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 an axiomatization that captures the behavior of the scoping operator and its interaction with the Kleene algebra operators and proved soundness over nominal languages. In this paper we show that the axioms are complete and describe the free language models.
2014-11-14T00:00:00ZMerlin: A Language for Provisioning Network ResourcesSoulé, RobertBasu, ShrutarshiMarandi, Parisa JaliliPedone, FernandoKleinberg, RobertSirer, Emin GünFoster, Natehttp://hdl.handle.net/1813/367052015-07-08T20:23:09Z2014-06-25T00:00:00ZMerlin: A Language for Provisioning Network Resources
Soulé, Robert; Basu, Shrutarshi; Marandi, Parisa Jalili; Pedone, Fernando; Kleinberg, Robert; Sirer, Emin Gün; Foster, Nate
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 predicates to identify sets of packets, regular expressions to encode forwarding paths, and arithmetic formulas to specify bandwidth constraints. The Merlin compiler uses a combination of advanced techniques to translate these policies into code that can be executed on network elements including a constraint solver that allocates bandwidth using parameterizable heuristics. To facilitate dynamic adaptation, Merlin provides mechanisms for delegating control of sub-policies and for verifying that modifications made to sub-policies do not violate global constraints. Experiments demonstrate the expressiveness and scalability of Merlin on real-world topologies and applications. Overall, Merlin simplifies network administration by providing high-level abstractions for specifying network policies and scalable infrastructure for enforcing them.
2014-06-25T00:00:00ZA Metrized Duality Theorem for Markov ProcessesKozen, DexterMardare, RaduPanangaden, Prakashhttp://hdl.handle.net/1813/363302015-07-08T09:37:59Z2014-05-21T00:00:00ZA Metrized Duality Theorem for Markov Processes
Kozen, Dexter; Mardare, Radu; Panangaden, Prakash
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 theorem become isometries in this quantitative setting. This opens the way to developing theories of approximate reasoning for probabilistic systems.
2014-05-21T00:00:00ZFine-Grained User Privacy from Avenance TagsBirrell, EleanorSchneider, Fred B.http://hdl.handle.net/1813/362852015-07-08T02:38:55Z2014-04-20T00:00:00ZFine-Grained User Privacy from Avenance Tags
Birrell, Eleanor; Schneider, Fred B.
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 notice and consent---are inadequate to address privacy needs of Internet users. This paper suggests a new, practical, and expressive policy tag scheme that would enable users to express both control-based and secrecy-based restrictions. We identify key design goals, explore various design choices that impact these goals, and outline a proposed implementation---called avenance tags---that realizes these goals.
2014-04-20T00:00:00ZA Hardware Design Language for Efficient Control of Timing ChannelsZhang, DanfengWang, YaoSuh, G. EdwardMyers, Andrew C.http://hdl.handle.net/1813/362742015-07-08T04:38:38Z2014-04-10T00:00:00ZA Hardware Design Language for Efficient Control of Timing Channels
Zhang, Danfeng; Wang, Yao; Suh, G. Edward; Myers, Andrew C.
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. We introduce a new hardware design language, SecVerilog, that in conjunction with software-level enforcement makes it possible to build systems in which timing channels and other leakage are verifiably controlled. SecVerilog extends Verilog with annotations that support comprehensive, precise reasoning about information flows at the hardware level. Compared to previous methods for designing secure hardware, SecVerilog offers a better tradeoff between expressiveness and run-time overhead. We demonstrate that it is expressive enough to build complex hardware designs, including a MIPS processor, with low overhead in time, space, and programmer effort. Information flow checking is mostly static, permitting hardware designs that are largely unaffected by security enforcement mechanisms. SecVerilog also tracks information at fine granularity, allowing interleaving of instructions and data at different security levels throughout the processor. SecVerilog also comes with stronger formal assurance than previous hardware design methods: we prove that it enforces noninterference, ensuring secure information flow.
Content file updated by author on 15 January 2015.
2014-04-10T00:00:00ZA Coalgebraic Decision Procedure for NetKATFoster, NateKozen, DexterMilano, MatthewSilva, AlexandraThompson, Laurehttp://hdl.handle.net/1813/362552015-07-08T20:22:13Z2014-03-26T00:00:00ZA Coalgebraic Decision Procedure for NetKAT
Foster, Nate; Kozen, Dexter; Milano, Matthew; Silva, Alexandra; Thompson, Laure
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 is undecidable in general, but in certain settings it is possible to develop domain-specific languages that are expressive enough to be practical and yet sufficiently restricted so that equivalence remains decidable.
In previous work we introduced NetKAT, a domain-specific language for specifying and verifying network packet-processing functions. NetKAT provides familiar constructs such as tests, assignments, union, sequential composition, and iteration as well as custom primitives for modifying packet headers and encoding network topologies. Semantically, NetKAT is based on Kleene algebra with tests (KAT) and comes equipped with a sound and complete equational theory. Although NetKAT equivalence is decidable, the best known algorithm is hardly practical-it uses Savitch's theorem to determinize a PSPACE algorithm and requires quadratic space.
This paper presents a new algorithm for deciding NetKAT equivalence. This algorithm is based on finding bisimulations between finite automata constructed from NetKAT programs. We investigate the coalgebraic theory of NetKAT, generalize the notion of Brzozowski derivatives to NetKAT, develop efficient representations of NetKAT automata in terms of spines and sparse matrices, and discuss the highlights of our prototype implementation.
2014-03-26T00:00:00ZKleene Algebra with EquationsKozen, DexterMamouras, Konstantinoshttp://hdl.handle.net/1813/362022015-07-08T11:46:12Z2014-02-27T00:00:00ZKleene Algebra with Equations
Kozen, Dexter; Mamouras, Konstantinos
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 approach to deductive completeness and coalgebraic decision procedures.
2014-02-27T00:00:00ZA Language for Securely Referencing Persistent Information in a Federated SystemLiu, JedMyers, Andrew C.http://hdl.handle.net/1813/351502015-07-08T02:40:55Z2014-01-17T00:00:00ZA Language for Securely Referencing Persistent Information in a Federated System
Liu, Jed; Myers, Andrew C.
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 integrity can itself lead to security vulnerabilities that are not currently well understood. This paper identifies three kinds of _referential security_ vulnerabilities related to the referential integrity of distributed, persistent information. Security conditions corresponding to the absence of these vulnerabilities are formalized. A language model is used to capture the key aspects of programming distributed systems with named, persistent resources in the presence of an adversary. The referential security of distributed systems is proved to be enforced by a new type system.
2014-01-17T00:00:00ZKAT + B!Grathwohl, Niels Bjørn BuggeKozen, DexterMamouras, Konstantinoshttp://hdl.handle.net/1813/348982015-07-08T11:08:41Z2014-01-08T00:00:00ZKAT + B!
Grathwohl, Niels Bjørn Bugge; Kozen, Dexter; Mamouras, Konstantinos
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 this extra feature in the form of mutable tests. The extension is conservative and is formulated as a general commutative coproduct construction. We give several results on deductive completeness and complexity of the system, as well as some examples of its use.
2014-01-08T00:00:00ZNetKAT: Semantic Foundations for NetworksAnderson, Carolyn JaneFoster, NateGuha, ArjunJeannin, Jean-BaptisteKozen, DexterSchlesinger, ColeWalker, Davidhttp://hdl.handle.net/1813/344452015-07-08T02:04:39Z2013-10-11T00:00:00ZNetKAT: Semantic Foundations for Networks
Anderson, Carolyn Jane; Foster, Nate; Guha, Arjun; Jeannin, Jean-Baptiste; Kozen, Dexter; Schlesinger, Cole; Walker, David
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 hardware than by foundational principles. The lack of a semantic foundation has left language designers with little guidance in determining how to incorporate new features, and programmers without a means to reason precisely about their code. This paper presents NetKAT, a new network programming language that is based on a solid mathematical foundation and comes equipped with a sound and complete equational theory. We describe the design of NetKAT, including primitives for filtering, modifying, and transmitting packets; operators for combining programs in parallel and in sequence; and a Kleene star operator for iteration. We show that NetKAT is an instance of a canonical and well studied mathematical structure called a Kleene algebra with tests (KAT) and prove that its equational theory is sound and complete with respect to its denotational semantics. Finally, we present practical applications of the equational theory including syntactic techniques for checking reachability properties, proving the correctness of compilation and optimization algorithms, and establishing a non-interference property that ensures isolation between programs.
2013-10-11T00:00:00ZToward General Diagnosis of Static Errors: Technical ReportZhang, DanfengMyers, Andrewhttp://hdl.handle.net/1813/337422015-07-08T02:55:03Z2013-08-22T00:00:00ZToward General Diagnosis of Static Errors: Technical Report
Zhang, Danfeng; Myers, Andrew
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 constraints. Given an unsatisfiable system of constraints, both satisfiable and unsatisfiable constraints are analyzed, to identify the program expressions most likely to be the cause of unsatisfiability. The likelihood of different error explanations is evaluated under the assumption that the programmer’s code is mostly correct, so the simplest error explanations are chosen, following Bayesian principles. For analyses that rely on programmer-stated assumptions, the diagnosis also identifies assumptions likely to have been omitted. The new error diagnosis approach has been implemented for two very different program analyses: type inference in OCaml and information flow checking in Jif. The effectiveness of the approach is evaluated using previously collected programs containing errors. The results show that the general technique identifies the location of program errors significantly more accurately than do existing compilers and other tools.
Content replaced at author's request on 2013-12-17.
2013-08-22T00:00:00ZInfinitary Axiomatization of the Equational Theory of Context-Free LanguagesGrathwohl, Niels Bjørn BuggeHenglein, FritzKozen, Dexterhttp://hdl.handle.net/1813/334172015-07-08T03:52:34Z2013-07-01T00:00:00ZInfinitary Axiomatization of the Equational Theory of Context-Free Languages
Grathwohl, Niels Bjørn Bugge; Henglein, Fritz; Kozen, Dexter
We give a natural complete infinitary axiomatization of the equational theory of the context-free languages, answering a question of Leiss (1992).
2013-07-01T00:00:00ZStrong Completeness for Markovian LogicsKozen, DexterMardare, RaduPanangaden, Prakashhttp://hdl.handle.net/1813/333802015-07-08T15:48:59Z2013-06-14T00:00:00ZStrong Completeness for Markovian Logics
Kozen, Dexter; Mardare, Radu; Panangaden, Prakash
In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, (ii) a logic for MPs defined for sub-probability distributions and (iii) a logic defined for arbitrary distributions.These logics are not compact so one needs infinitary rules in order to obtain strong completeness results.
We propose a new infinitary rule that replaces the so-called Countable Additivity Rule (CAR) currently used in the literature to address the problem of proving strong completeness for these and similar logics. Unlike the CAR, our rule has a countable set of instances; consequently it allows us to apply the Rasiowa-Sikorski lemma for establishing strong completeness. Our proof method is novel and it can be used for other logics as well.
2013-06-14T00:00:00ZScalable Network Management with MerlinSoulé, RobertBasu, ShrutarshiSirer, Emin GünFoster, Natehttp://hdl.handle.net/1813/333792015-07-08T08:19:21Z2013-06-13T00:00:00ZScalable Network Management with Merlin
Soulé, Robert; Basu, Shrutarshi; Sirer, Emin Gün; Foster, Nate
This paper presents the Merlin network management framework. With Merlin, network administrators express functionality such as accounting, bandwidth provisioning, and traffic filtering in a high-level policy language, and use automated tools and mechanisms to implement them. The framework includes: (i) a declarative language for specifying policies, (ii) infrastructure for distributing, refining, and coordinating enforcement of policies, and (iii) a run-time monitor that inspects incoming and outgoing traffic on end hosts. We describe Merlin's policy language and enforcement infrastructure, illustrate the use of Merlin on case studies, and present experimental results demonstrating that Merlin is more efficient and scalable than equivalent implementations based on programmable switches and centralized middleboxes. Overall, Merlin simplifies the task of network administration by providing high-level abstractions and tools for specifying and enforcing rich network policies.
2013-06-13T00:00:00ZWell-Founded Coalgebras, RevisitedJeannin, Jean-BaptisteKozen, DexterSilva, Alexandrahttp://hdl.handle.net/1813/333302015-07-08T03:11:34Z2013-05-24T00:00:00ZWell-Founded Coalgebras, Revisited
Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra
Theoretical models of recursion schemes have been well studied under the names well-founded coalgebras, recursive coalgebras, corecursive algebras, and Elgot algebras. Much of this work focuses on conditions ensuring unique or canonical solutions, e.g. when the coalgebra is well-founded. If the coalgebra is not well-founded, then there can be multiple solutions. The standard semantics of recursive programs gives a particular solution, namely the least solution in a flat Scott domain, which may not be the desired one. We have recently proposed programming language constructs to allow the specification of alternative solutions and methods to compute them. We have implemented these new constructs as an extension of OCaml. In this paper, we prove some theoretical results characterizing well-founded coalgebras that slightly extend results of Adamek, Luecke, and Milius (2007), along with several examples for which this extension is useful. We also give several examples that are not well-founded but still have a desired solution. In each case, the function would diverge under the standard semantics of recursion, but can be specified and computed with the programming language constructs we have proposed.
2013-05-24T00:00:00ZWhen not all bits are equal: Worth-based information flowAlvim, Mário S.Scedrov, AndreSchneider, Fred B.http://hdl.handle.net/1813/331242015-07-08T08:22:48Z2013-04-01T00:00:00ZWhen not all bits are equal: Worth-based information flow
Alvim, Mário S.; Scedrov, Andre; Schneider, Fred B.
Only recently have approaches to quantitative information flow started to challenge the presumption that all leaks involving a given number of bits are equally harmful. This paper proposes a framework to capture the semantics of information, making quantification of leakage independent of the syntactic representation of secrets. Secrets are defined in terms of fields, which are combined to form structures; and a worth assignment is introduced to associate each structure with a worth (perhaps in proportion to the harm that would result from disclosure). We show how worth assignments can capture inter dependence among structures within a secret, modeling: (i) secret sharing, (ii) information-theoretic predictors, and (iii) computational (as opposed to information-theoretic) guarantees for security. Using non-trivial worth assignments, we generalize Shannon entropy, guessing entropy, and probability of guessing. For deterministic systems, we give a lattice of information to provide an underlying algebraic structure for the composition of attacks. Finally, we outline a design technique to capture into worth assignments relevant aspects of a scenario of interest.
Content replaced at author's request on 2014-02-12.
2013-04-01T00:00:00ZReconciling Exhaustive Pattern Matching with ObjectsIsradisaikul, ChinawatMyers, Andrew C.http://hdl.handle.net/1813/331232015-07-08T02:44:50Z2013-03-29T00:00:00ZReconciling Exhaustive Pattern Matching with Objects
Isradisaikul, Chinawat; Myers, Andrew C.
Pattern matching, an important feature of functional languages, is in
conflict with data abstraction and extensibility, which are central to
object-oriented languages. Modal abstraction offers an integration of
deep pattern matching and convenient iteration abstractions into an
object-oriented setting; however, because of data abstraction, it is
challenging for a compiler to statically verify properties such as
exhaustiveness. In this work, we extend modal abstraction in the
JMatch language to support static, modular reasoning about
exhaustiveness and redundancy. New matching specifications allow
these properties to be checked using an SMT solver. We also introduce
expressive pattern-matching constructs. Our evaluation shows
that these new features enable more
concise code and that the performance of checking exhaustiveness
and redundancy is acceptable.
2013-03-29T00:00:00ZStone Duality for Markov ProcessesKozen, DexterLarsen, Kim G.Mardare, RaduPanangaden, Prakashhttp://hdl.handle.net/1813/315652015-07-07T22:43:55Z2013-03-14T00:00:00ZStone Duality for Markov Processes
Kozen, Dexter; Larsen, Kim G.; Mardare, Radu; Panangaden, Prakash
We define Aumann algebras, an algebraic analog of probabilistic modal logic. An Aumann algebra consists of a Boolean algebra with operators modeling probabilistic transitions. We prove that countable Aumann algebras and countably-generated continuous-space Markov processes are dual in the sense of Stone. Our results subsume existing results on completeness of probabilistic modal logics for Markov processes.
2013-03-14T00:00:00ZTyped Kleene Algebra with Products and Iteration TheoriesKozen, DexterMamouras, Konstantinoshttp://hdl.handle.net/1813/313722015-07-08T15:18:23Z2013-02-22T00:00:00ZTyped Kleene Algebra with Products and Iteration Theories
Kozen, Dexter; Mamouras, Konstantinos
We develop a typed equational system that subsumes both iteration theories and typed Kleene algebra in a common framework. Our approach is based on cartesian categories endowed with commutative strong monads to handle nondeterminism.
2013-02-22T00:00:00ZCoCaml: Programming with Coinductive TypesJeannin, Jean-BaptisteKozen, DexterSilva, Alexandrahttp://hdl.handle.net/1813/307982015-07-08T00:26:32Z2012-12-31T00:00:00ZCoCaml: Programming with Coinductive Types
Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra
We present CoCaml, a functional programming language extending OCaml, which allows us to define
functions on coinductive datatypes parameterized by an equation solver. We provide numerous examples that attest to the usefulness of the new programming constructs, including operations on infinite lists, infinitary lambda-terms and p-adic numbers.
2012-12-31T00:00:00ZPractical CoinductionKozen, DexterSilva, Alexandrahttp://hdl.handle.net/1813/305102015-07-07T23:25:12Z2012-11-11T00:00:00ZPractical Coinduction
Kozen, Dexter; Silva, Alexandra
Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively-defined datatypes such as finite lists, finite trees, and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes.
2012-11-11T00:00:00ZFederated Identity Management Systems: A Privacy-based CharacterizationBirrell, EleanorSchneider, Fred B.http://hdl.handle.net/1813/304712015-07-08T01:55:10Z2012-10-16T00:00:00ZFederated Identity Management Systems: A Privacy-based Characterization
Birrell, Eleanor; Schneider, Fred B.
Identity management systems store attributes associated with users and facilitate authorization on the basis of these attributes. A privacy-driven characterization of the principal design choices for identity management systems is given, and existing systems are fit into this framework. The taxonomy of design choices also can guide public policy relating to identity management, which is illustrated using the United States NSTIC initiative.
2012-10-16T00:00:00ZConstant-Round Concurrent Zero-Knowledge From Falsifiable AssumptionsChung, Kai-MinLin, HuijiaPass, Rafaelhttp://hdl.handle.net/1813/303982015-07-08T10:34:51Z2012-10-02T00:00:00ZConstant-Round Concurrent Zero-Knowledge From Falsifiable Assumptions
Chung, Kai-Min; Lin, Huijia; Pass, Rafael
We present a constant-round concurrent zero-knowledge protocol for $\NP$. Our protocol is sound against uniform polynomial-time attackers, and relies on the existence of families of collision-resistant hash functions, and a new (but in our eyes, natural) falsifiable intractability assumption: Roughly speaking, that Micali's non-interactive CS-proofs are sound for languages in $\P$.
2012-10-02T00:00:00ZReflection in the Chomsky HierarchyBarendregt, HenkCapretta, VenanzioKozen, Dexterhttp://hdl.handle.net/1813/296122015-07-08T02:49:49Z2012-07-31T00:00:00ZReflection in the Chomsky Hierarchy
Barendregt, Henk; Capretta, Venanzio; Kozen, Dexter
We investigate which classes of formal languages in the Chomsky hierarchy are reflexive, that is, contain a language of codes that is universal for the whole class.
2012-07-31T00:00:00ZCosts of Security in the PFS File SystemWalsh, KevinSchneider, Fredhttp://hdl.handle.net/1813/296092015-07-08T06:29:04Z2012-07-25T00:00:00ZCosts of Security in the PFS File System
Walsh, Kevin; Schneider, Fred
Various principles have been proposed for the design of trustworthy systems. But there is little data about their impact on system performance. A filesystem that pervasively instantiates a number of well-known security principles was implemented and the performance impact of various design choices was analyzed. The overall performance of this filesystem was also compared to a Linux filesystem that largely ignores the security principles.
2012-07-25T00:00:00ZNetSlices: Scalable Multi-Core Packet Processing in User-SpaceMarian, TudorLee, Ki SuhWeatherspoon, Hakimhttp://hdl.handle.net/1813/295432015-07-08T00:45:28Z2012-07-18T00:00:00ZNetSlices: Scalable Multi-Core Packet Processing in User-Space
Marian, Tudor; Lee, Ki Suh; Weatherspoon, Hakim
Modern commodity operating systems do not provide developers with user-space abstractions for building high-speed packet processing applications. The conventional raw socket is inefficient and unable to take advantage of the emerging hardware, like multi-core processors and multi-queue network adapters. In this paper we present the NetSlice operating system abstraction. Unlike the conventional raw socket, NetSlice tightly couples the hardware and software packet processing resources, and provides the application with control over these resources. To reduce shared resource contention, NetSlice performs domain specific, coarse-grained, spatial partitioning of CPU cores, memory, and NICs. Moreover, it provides a streamlined communication channel between NICs and user-space. Although backward compatible with the conventional socket API, the \netslice API also provides batched (multi-) send/receive operations to amortize the cost of protection domain crossings. We show that complex user-space packet processors---like a protocol accelerator and an IPsec gateway---built from commodity components can scale linearly with the number of cores and operate at 10Gbps network line speeds.
2012-07-18T00:00:00ZFlexAura SchematicsShenwei, Liuhttp://hdl.handle.net/1813/290872015-09-02T16:18:21Z2012-06-21T00:00:00ZFlexAura Schematics
Shenwei, Liu
Schematics of our sensor and the control board.
2012-06-21T00:00:00ZCommodifying Replicated State Machines with OpenReplicaAltinbuken, DenizSirer, Emin Gunhttp://hdl.handle.net/1813/290092015-07-08T07:49:42Z2012-06-05T00:00:00ZCommodifying Replicated State Machines with OpenReplica
Altinbuken, Deniz; Sirer, Emin Gun
This paper describes OpenReplica, an open service that
provides replication and synchronization support for
large-scale distributed systems. OpenReplica is designed
to commodify Paxos replicated state machines by providing infrastructure for their construction, deployment and
maintenance. OpenReplica is based on a novel Paxos
replicated state machine implementation that employs an
object-oriented approach in which the system actively
creates and maintains live replicas for user-provided objects. Clients access these replicated objects transparently as if they are local objects. OpenReplica supports
complex distributed synchronization constructs through
a multi-return mechanism that enables the replicated objects to control the execution ﬂow of their clients, in
essence providing blocking and non-blocking method invocations that can be used to implement richer synchronization constructs. Further, it supports elasticity requirements of cloud deployments by enabling any number of servers to be replaced dynamically. A rack-aware
placement manager places replicas on nodes that are unlikely to fail together. Experiments with the system show
that the latencies associated with replication are comparable to ZooKeeper, and that the system scales well.
2012-06-05T00:00:00ZPolynomial Time Construction for Spatially Balanced Latin SquaresLe Bras, RonanPerrault, AndrewGomes, Carla P.http://hdl.handle.net/1813/286972015-07-08T02:49:40Z2012-04-17T00:00:00ZPolynomial Time Construction for Spatially Balanced Latin Squares
Le Bras, Ronan; Perrault, Andrew; Gomes, Carla P.
In this paper we propose a construction that generates spatially balanced
Latin squares (SBLSs) in polynomial time. These structures are central to
the design of agronomic experiments, as they avoid biases that are otherwise
unintentionally introduced due to spatial auto-correlation. Previous
approaches were able to generate SBLSs of order up to 35 and required
about two weeks of computation. Our algorithm runs in O(n2) and generates
SBLSs of arbitrary order n where 2n + 1 is prime. For example, this
algorithm generates a SBLS of order 999 in a fraction of a second.
2012-04-17T00:00:00ZThe Triumph of Types: Principia Mathematica's Impact on Computer ScienceConstable, Roberthttp://hdl.handle.net/1813/286962015-07-08T04:08:50Z2011-07-16T00:00:00ZThe Triumph of Types: Principia Mathematica's Impact on Computer Science
Constable, Robert
Types now play an essential role in computer science; their ascent originates from Principia Mathematica. Type checking and type inference algorithms are used to prevent semantic errors in programs, and type theories are the native language of several major interactive theorem provers. Some of these trace key features back to Principia.
This lecture examines the in°uence of Principia Mathematica on modern type theories implemented in software systems known as interactive proof assistants. These proof assistants advance daily the goal for which Principia was designed: to provide a comprehensive formalization of mathematics. For instance, the de¯nitive formal proof of the Four Color Theorem was done in type theory. Type theory is considered seriously now more than ever as an adequate foundation for both classical and constructive mathematics as well as for computer science. Moreover, the seminal work in the history of formalized mathematics is the Automath project of N.G. de Bruijn whose formalism is type theory. In addition we explain how type theories have enabled the use of formalized mathematics as a practical programming language, a connection entirely unanticipated at the time of Principia Mathematica's creation.
Video available as the last entry on the Oregon Programming Languages Summer School - curriculum page: http://www.cs.uoregon.edu/Research/summerschool/summer11/curriculum.html
2011-07-16T00:00:00ZThe Logic of Events, a framework to reason about distributed systemsBickford, MarkConstable, RobertRahli, Vincenthttp://hdl.handle.net/1813/286952015-07-08T04:08:49Z2012-01-23T00:00:00ZThe Logic of Events, a framework to reason about distributed systems
Bickford, Mark; Constable, Robert; Rahli, Vincent
We present a logical framework to reason
about distributed systems called the Logic of Events. This logic has been formalized in Nuprl. We developed a suite of tools and tactics in Nuprl to reason about event classes. We also developed a programming language called EventML which allows programmers to write specifications of distributed protocols.
2012-01-23T00:00:00ZLanguage Mechanisms for Controlling and Mitigating Timing ChannelsZhang, DanfengAskarov, AslanMyers, Andrewhttp://hdl.handle.net/1813/286352015-07-08T01:50:59Z2012-03-22T00:00:00ZLanguage Mechanisms for Controlling and Mitigating Timing Channels
Zhang, Danfeng; Askarov, Aslan; Myers, Andrew
We propose a new language-based approach to mitigating timing channels. In this language, well-typed programs provably leak only a bounded amount of information over time through external timing channels. By incorporating mechanisms for predictive mitigation of timing channels, this approach also permits a more expressive programming model. Timing channels arising from interaction with underlying hardware features such as instruction caches are
controlled. Assumptions about the underlying hardware are explicitly formalized, supporting the design of hardware that efficiently controls timing channels. One such hardware design is modeled
and used to show that timing channels can be controlled in some simple programs of real-world significance.
2012-03-22T00:00:00ZNewKozen, Dexterhttp://hdl.handle.net/1813/286322015-07-08T00:15:40Z2012-03-17T00:00:00ZNew
Kozen, Dexter
We propose a theoretical device for modeling the creation of new indiscernible semantic objects during program execution. The method fits well with the semantics of imperative, functional, and object-oriented languages and promotes equational reasoning about higher-order state.
2012-03-17T00:00:00ZCapsules and SeparationJeannin, Jean-BaptisteKozen, Dexterhttp://hdl.handle.net/1813/282842015-07-07T22:32:01Z2012-01-14T00:00:00ZCapsules and Separation
Jeannin, Jean-Baptiste; Kozen, Dexter
We study a formulation of separation logic using capsules, a representation of the state of a computation in higher-order programming languages with mutable variables. We prove soundness of the frame rule in this context and investigate alternative formulations with weaker side conditions.
2012-01-14T00:00:00ZIntuitionistic Completeness of First-Order LogicConstable, RobertBickford, Markhttp://hdl.handle.net/1813/243982015-07-08T06:28:33Z2011-10-07T00:00:00ZIntuitionistic Completeness of First-Order Logic
Constable, Robert; Bickford, Mark
We establish completeness for intuitionistic first-order logic, iFOL, showing that is a formula is provable if and only if it is uniformly valid under the Brouwer Heyting Kolmogorov (BHK) semantics, the intended semantics of iFOL. Our proof is intuitionistic and provides an effective procedure Prf that converts uniform evidence into a formal first-order proof. We have implemented Prf . Uniform validity is defined using the intersection operator as a universal quantifier over the domain of discourse and atomic predicates. Formulas of iFOL that are uniformly valid are also intuitionistically valid, but not conversely. Our strongest result requires the Fan Theorem; it can also be proved classically by showing that Prf terminates using K¨onig’s Theorem.
The fundamental idea behind our completeness theorem is that a single evidence term evd witnesses the uniform validity of a minimal logic formula F. Finding even one uniform realizer guarantees validity because Prf (F, evd) builds a first-order proof of F, establishing its uniform validity and providing a purely logical normalized realizer.
We establish completeness for iFOL as follows. Friedman showed that iFOL can be embedded in minimal logic (mFOL). By his transformation, mapping formula A to F r(A). If A is uniformly valid, then so is F r(A), and by our Basic Completeness result, we can find a proof of F r(A) in minimal logic. Then we prove A from F r(A) in intuitionistic logic by a proof procedure fixed in advance. Our result resolves an open question posed by Beth in 1947.
2011-10-07T00:00:00Z