Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories. We address this issue by designing a dependently typed language where equality checking is delayed until runtime. What were once static errors can now be presented to programmers as warnings. When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution. We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language. Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage. Finally, we have implemented a prototype of the language.

Investigating the nature of system intrusions in large distributed systems remains a notoriously difficult challenge. While monitoring tools (e.g., Firewalls, IDS) provide preliminary alerts through easy-to-use administrative interfaces, attack reconstruction still requires that administrators sift through gigabytes of system audit logs stored locally on hundreds of machines. At present, two fundamental obstacles prevent synergy between system-layer auditing and modern cluster monitoring tools: 1) the sheer volume of audit data generated in a data center is prohibitively costly to transmit to a central node, and 2) system-layer auditing poses a "needle-in-a-haystack" problem, such that hundreds of employee hours may be required to diagnose a single intrusion. This paper presents Winnower, a scalable system for audit-based cluster monitoring that addresses these challenges. Our key insight is that, for tasks that are replicated across nodes in a distributed application, a model can be defined over audit logs to succinctly summarize the behavior of many nodes, thus eliminating the need to transmit redundant audit records to a central monitoring node. Specifically, Winnower parses audit records into provenance graphs that describe the actions of individual nodes, then performs grammatical inference over individual graphs using a novel adaptation of Deterministic Finite Automata (DFA) Learning to produce a behavioral model of many nodes at once. This provenance model can be efficiently transmitted to a central node and used to identify anomalous events in the cluster. We have implemented Winnower for Docker Swarm container clusters and evaluate our system against real-world applications and attacks. We show that Winnower dramatically reduces storage and network overhead associated with aggregating system audit logs, by as much as 98%, without sacrificing the important information needed for attack investigation. Winnower thus represents a significant step forward for security monitoring in distributed systems.

Container-based virtualization is enabling unprecedented portability and deployment of code, facilitated by online registries like Docker Store and cluster management tools like Docker Swarm. However, present day audit mechanisms were not designed for this emerging paradigm, especially in large-scale clusters of container deployments where the sheer scale of storing and processing audit logs makes system monitoring prohibitively costly. In this poster, we consider a unique adaptation of Regular Grammar principles that enables us to define a provenance model for a container's expected behavior, and subsequently prune all but the unique/anomalous behaviors of a particular container instance. We consider the performance of such an approach, as well as real-world attack scenarios in which this approach enables cluster-wide monitoring of containers.

Provenance collection techniques have been carefully studied in the literature, and there are now several systems to automatically capture provenance data. However, the analysis of provenance data is often left "as an exercise for the reader". The provenance community needs tools that allow users to quickly sort through large volumes of provenance data and identify records that require further investigation. By detecting anomalies in provenance data that deviate from established patterns, we hope to actively thwart security threats. In this paper, we discuss issues with current graph analysis techniques as applied to data provenance, particularly Frequent Subgraph Mining (FSM). Then we introduce Directed Acyclic Graph regular grammars (DAGr) as a model for provenance data and show how they can detect anomalies. These DAGr provide an expressive characterization of DAGs, and by using regular grammars as a formalism, we can apply results from formal language theory to learn the difference between "good" and "bad" provenance. We propose a restricted subclass of DAGr called deterministic Directed Acyclic Graph automata (dDAGa) that guarantees parsing in linear time. Finally, we propose a learning algorithm for dDAGa, inspired by Minimum Description Length for Grammar Induction [1].