http://hdl.handle.net/1813/5602 Wed, 08 May 2013 00:39:05 GMT 2013-05-08T00:39:05Z http://hdl.handle.net/1813/33124 Title: When not all bits are equal: Incorporating "worth" into information-flow measures Authors: Alvim, Mário S.; Scedrov, Andre; Schneider, Fred B. Abstract: Approaches to quantitative information flow (QIF) traditionally have presumed that all leaks involving a given number of bits are equally harmful. The presumption is unrealistic, so a new approach to QIF is described. Here, secrets are defined in terms of fields, where derived secrets obtained by combining these fields can be assigned a different “worth” (perhaps in proportion to the harm that would result from disclosure). New measures that incorporate worth into QIF are then defined; they generalize probability of guessing, guessing entropy, and Shannon entropy. A lattice of information is derived to provide an underlying algebraic structure for an adversary’s state of knowledge in this more-general setting. Mon, 01 Apr 2013 00:00:00 GMT http://hdl.handle.net/1813/33124 2013-04-01T00:00:00Z http://hdl.handle.net/1813/33123 Title: Reconciling Exhaustive Pattern Matching with Objects Authors: Isradisaikul, Chinawat; Myers, Andrew C. Abstract: 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. Fri, 29 Mar 2013 00:00:00 GMT http://hdl.handle.net/1813/33123 2013-03-29T00:00:00Z http://hdl.handle.net/1813/31565 Title: Stone Duality for Markov Processes Authors: Kozen, Dexter; Larsen, Kim G.; Mardare, Radu; Panangaden, Prakash Abstract: 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. Thu, 14 Mar 2013 00:00:00 GMT http://hdl.handle.net/1813/31565 2013-03-14T00:00:00Z http://hdl.handle.net/1813/31372 Title: Typed Kleene Algebra with Products and Iteration Theories Authors: Kozen, Dexter; Mamouras, Konstantinos Abstract: 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. Fri, 22 Feb 2013 00:00:00 GMT http://hdl.handle.net/1813/31372 2013-02-22T00:00:00Z http://hdl.handle.net/1813/30798 Title: CoCaml: Programming with Coinductive Types Authors: Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra Abstract: 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. Mon, 31 Dec 2012 00:00:00 GMT http://hdl.handle.net/1813/30798 2012-12-31T00:00:00Z http://hdl.handle.net/1813/30510 Title: Practical Coinduction Authors: Kozen, Dexter; Silva, Alexandra Abstract: 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. Sun, 11 Nov 2012 00:00:00 GMT http://hdl.handle.net/1813/30510 2012-11-11T00:00:00Z http://hdl.handle.net/1813/30471 Title: Federated Identity Management Systems: A Privacy-based Characterization Authors: Birrell, Eleanor; Schneider, Fred B. Abstract: 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. Tue, 16 Oct 2012 00:00:00 GMT http://hdl.handle.net/1813/30471 2012-10-16T00:00:00Z http://hdl.handle.net/1813/30398 Title: Constant-Round Concurrent Zero-Knowledge From Falsifiable Assumptions Authors: Chung, Kai-Min; Lin, Huijia; Pass, Rafael Abstract: 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$. Tue, 02 Oct 2012 00:00:00 GMT http://hdl.handle.net/1813/30398 2012-10-02T00:00:00Z http://hdl.handle.net/1813/29612 Title: Reflection in the Chomsky Hierarchy Authors: Barendregt, Henk; Capretta, Venanzio; Kozen, Dexter Abstract: 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. Tue, 31 Jul 2012 00:00:00 GMT http://hdl.handle.net/1813/29612 2012-07-31T00:00:00Z http://hdl.handle.net/1813/29609 Title: Costs of Security in the PFS File System Authors: Walsh, Kevin; Schneider, Fred Abstract: 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. Wed, 25 Jul 2012 00:00:00 GMT http://hdl.handle.net/1813/29609 2012-07-25T00:00:00Z