Computing and Information Sciencehttp://hdl.handle.net/1813/3582016-02-10T20:17:42Z2016-02-10T20:17:42ZKolmogorov 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:00ZFull-Processor Timing Channel Protection with Applications to Secure Hardware CompartmentsFerraiuolo, AndrewWang, YaoXu, RuiZhang, DanfengMyers, AndrewSuh, Edwardhttp://hdl.handle.net/1813/412182015-11-11T06:02:12Z2015-01-01T00: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.
2015-01-01T00:00:00ZRegular Expressions with Dynamic Name BindingKozen, DexterMilius, StefanSchröder, LutzWißmann, Thorstenhttp://hdl.handle.net/1813/411882015-10-19T05:00:47Z2015-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.
2015-10-18T00:00:00ZElection Verifiability: Cryptographic Definitions and an Analysis of Helios and JCJSmyth, BenFrink, StevenClarkson, Michael R.http://hdl.handle.net/1813/405752015-08-07T05:01:06Z2015-08-06T00: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.
2015-08-06T00: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:00ZGenus: Making Generics Object-Oriented, Expressive, and LightweightZhang, YizhouLoring, Matthew C.Salvaneschi, GuidoLiskov, BarbaraMyers, Andrew C.http://hdl.handle.net/1813/399102015-07-08T04:32:39Z2015-04-15T00: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-04-15T00: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:00Z