Kenn Knowles - Publications & Projects

Faceted Dynamic Information Flow via Control and Data Monads

Thomas Schmitz, Dustin Rhodes, Thomas H. Austin, Kenneth Knowles, Cormac Flanagan
Principles of Security and Trust, 2016
(PDF code)
Abstract: An application that fails to ensure information flow security may leak sensitive data such as passwords, credit card numbers, or medical records. News stories of such failures abound. Austin and Flanagan introduce faceted values – values that present different behavior according to the privilege of the observer – as a dynamic approach to enforce information flow policies for an untyped, imperative λ-calculus.

We implement faceted values as a Haskell library, elucidating their relationship to types and monadic imperative programming. In contrast to previous work, our approach does not require modification to the language runtime. In addition to pure faceted values, our library supports faceted mutable reference cells and secure facet-aware socket-like communication. This library guarantees information flow security, independent of any vulnerabilities or bugs in application code. The library uses a control monad in the traditional way for encapsulating effects, but it also uniquely uses a second data monad to structure faceted values. To illustrate a non-trivial use of the library, we present a bi-monadic interpreter for a small language that illustrates the interplay of the control and data monads.

Executable Refinement Types

Kenneth Knowles.
Doctoral Dissertation, 2014.
My dissertation incorporates and expands upon all of my research to date on refinement types. I present a new exposition of the ideas in a uniform notation, as panel panel-info a thorough treatment of prior work, technical prerequisites, and an extended discussion of ongoing related research trends.

Bikes In / Bikes Out

Kenneth Knowles, Zia Sobhani, Verena Tiefenbeck, Kim Ducharme.
Hubway Data Visualization Challenge, 2012.
Awarded Best Analysis.
(Interactive visualization)
Abstract: Our visualization makes it extremely clear that Hubway - the greater Boston area's bike share system - is not just a tourist attraction but serves a large number of commuters as part of the greater Boston area's public transit infrastructure (it is also great for tourists). Use is very high at stations near transit hubs, especially South & North Station, suggesting that many commuters include it in mixed-mode trips with the T and commuter rail. The heavy use at stations that are very near to each other also demonstrates that the dense network of stations is important to the system.

Hybrid Type Checking

Kenneth Knowles, Cormac Flanagan.
Transactions on Programming Languages and Systems, 2010.
Abstract: Traditional static type systems are effective for verifying basic interface specifications. Dynamically checked contracts support more precise specifications, but these are not checked until run time, resulting in incomplete detection of defects. Hybrid type checking is a synthesis of these two approaches that enforces precise interface specifications, via static analysis where possible, but also via dynamic checks where necessary. This paper explores the key ideas and implications of hybrid type checking, in the context of the λ-calculus extended with contract types, i.e., with dependent function types and with arbitrary refinements of base types.

Compositional and Decidable Checking for Dependent Contract Types

Kenneth Knowles, Cormac Flanagan.
Programming Languages meets Program Verification, 2009.
Abstract: Simple type systems perform compositional reasoning in that the type of a term depends only on the types of its subterms, and not on their semantics. Contracts offer more expressive abstractions, but static contract checking systems typically violate those abstractions and base their reasoning directly upon the semantics of terms. Pragmatically, this noncompositionality makes the decidability of static checking unpredictable.

We first show how compositional reasoning may be restored using standard type-theoretic techniques, namely existential types and subtyping. Despite its compositional nature, our type system is exact, in that the type of a term can completely capture its semantics, hence demonstrating that precision and compositionality are compatible. We then address predictability of static checking for contract types by giving a type-checking algorithm for an im- portant class of programs with contract predicates drawn from a decidable theory. Our algorithm relies crucially on the fact that the type of a term depends only the types of its subterms (which fall into the decidable theory) and not their semantics (which will not, in general).

Proving correctness of a dynamic atomicity analysis in Coq

Caitlin Sadowski, Jaeheon Yi, Kenneth Knowles, Cormac Flanagan.
Workshop on Mechanizing Metatheory, 2008.
(PDF Coq)
Abstract: Writing and reasoning about concurrent programs remains notoriously dicult despite the proliferation of type systems, static analyses, and dynamic analyses targeting concurrent programs. There are examples of veried developments for concurrent languages and programs but most analyses - especially dynamic analyses - have not been subjected to mechanical rigor. We report on our partial mechanization in Coq of the recently released Velodrome dynamic atomicity checker.

First-Order Logic à la Carte

Kenneth Knowles.
The Monad Reader Issue 11, 2008.
Abstract: Classical first-order logic has the pleasant property that a formula can be reduced to an elegant implicative normal form through a series of syntactic simplifications. Using these transformations as a vehicle, this article demonstrates how to use Haskell’s type system, specifically a variation on Swierstra’s “Data Types à la Carte” method, to enforce the structural correctness property that these constructors are, in fact, eliminated by each stage of the transformation.

Type Reconstruction for General Refinement Types.

Kenneth Knowles, Cormac Flanagan.
European Symposium on Programming, 2007.
(PDF extended)
Abstract: General refinement types allow types to be refined by predicates written in a general-purpose programming language, and can express function preconditions and postconditions and data structure invariants. In this setting, with expressive and possibly verbose types, type reconstruction is particularly valuable, yet typeability is undecidable because it subsumes type checking. Using a generalized notion of type reconstruction, we present the first type reconstruction algorithm for a type system with base types refined by abitrary program terms. Our algorithm is a typeability-preserving transformation and defers type checking to a subsequent phase. The algorithm generates and solves a collection of implication constraints over refinement predicates, inferring maximally precise refinement predicates in a largely syntactic manner that is reminiscent of strongest postcondition calculation. Perhaps surprisingly, our notion of type reconstruction is decidable even though type checking is not.

Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic.

Kenneth Knowles, Aaron Tomb, Jessica Gronski, Cormac Flanagan, Stephen Freund.
Workshop on Scheme and Functional Programming, 2006.
(PDF website)
Abstract: Software systems typically contain large APIs that are informally specified and hence easily misused. This paper presents the Sage programming language, which is designed to enforce precise interface specifications in a flexible manner. The Sage type system uses a synthesis of the type Dynamic, first-class types, and arbitrary refinement types. Since type checking for this expressive language is not statically decidable, Sage uses hybrid type checking, which extends static type checking with dynamic contract checking, automatic theorem proving, and a database of refuted subtype judgments.