Selected Research Projects
Network protocols such as TLS can be customized through a vast array of options with unpredictable interactions and dangerous security implications. We are developing accountable protocol customization, a framework that combines synthesis, testing, and verification techniques to extract backward-compatible, lean protocol subsets while meeting realistic functional and security requirements. Our ultimate goal is to target widely used standards for network infrastructure, secure messaging, federated authentication, and the Internet of Things.
Prevalent software engineering practices have significantly increased the complexity and bloat of today’s software. This bloat has led to decreased performance and increased security vulnerabilities. The ASPIRE project seeks to develop a toolkit and methodology to effectively counter this trend. Bloat reduction poses significant challenges that ASPIRE endeavors to address. ASPIRE aims for a fully automated reduction process that can handle legacy source and binary code, and scale to large, complex programs that implement protocols.
STRANDS is a declarative programming-based framework for verification and debugging of distributed systems, allowing for static analysis of the system specification and runtime analysis of the system implementation. STRANDS relies on Network Datalog (NDlog) for system modeling and programming. NDlog is a declarative programming language for network protocols, extending the classical query language Datalog.
The goal of the DeDOS project is to create fundamentally new defenses against distributed denial-of-service (DDoS) attacks that can provide far greater resilience to these attacks compared to existing solutions. Today’s responses to DDoS attacks largely rely on old-school network-based filtering or scrubbing, which are slow and manual, and cannot handle new attacks. DeDOS takes a radically different approach that combines techniques from declarative programming, program analysis, and real-time resource allocation in the cloud.
The overall research objective is to combine big data analytics with econometric techniques and social psychology user studies, to enhance our fundamental understanding of how early-stage high-tech startups operate – and how we might model (and optimize) their behavior and decision processes. This project is in collaboration with Wharton School.
NetPoirot: Failure Diagnosis for Data-center Networks
Today, root cause analysis of failures in data centers is mostly done through manual inspection. More often than not customers blame the network as the culprit. However, other components of this system might have caused these failures. This project aims to develop a lightweight, accurate, non-intrusive tool for infering about failures in the data center using TCP statistics collected at endpoints.
NetEgg is a programming tool that allows network operators who may not be trained in programming to develop network policies by describing representative example behaviors. Given these scenarios, a synthesis algorithm automatically infers the controller state that needs to be maintained along with the rules to process network events and update state.
The goal of ExCAPE is to transform the way programmers develop software by advancing the theory and practice of software synthesis. In the proposed paradigm, a programmer can express insights through a variety of forms such as incomplete programs, example behaviors, and high-level requirements, and the synthesis tool generates the implementation relying on powerful analysis algorithms and programmer collaboration.
The goal of this project is to provide secure network provenance, that is, the ability to correctly explain system states even when (and especially when) the system is faulty or under attack. Towards this goal, we are substantially extending and generalizing the concept of network provenance by adding capabilities needed in a forensic setting, we are developing techniques for securely storing provenance without trusted components, and we are designing methods for efficiently querying secure provenance. We are evaluating our techniques in the context of concrete applications, such as Hadoop MapReduce or BGP interdomain routing.
NEBULA is a future Internet architecture that is intrinsically more secure and addresses threats to the emerging computer utility capabilities (called cloud computing) while meeting the challenges of flexibility, extensibility and economic viability.
Interdomain routing protocol stability depends on the absence of policy conflicts between autonomous systems; but since most policy is kept private, it is hard to ensure that conflicts are avoided. We show that even limited information can be used to help guide network (re-)configuration, by automated tools that assist network operators. This work is based on an underlying formalism of partially specified policy configurations, which has related applications in network optimization, resilience, and giving insight.
Cologne is a declarative optimization platform that enables constraint optimization problems (COPs) to be declaratively speciï¬ed and incrementally executed in distributed systems. Cologne integrates the RapidNet declarative networking engine with the Gecode constraint solver. Cologne uses the Colog declarative language that combines distributed Datalog used in declarative networking with language constructs for concisely specifying goals and constraints used in COPs. The Cologne platform has tremendous practical value in facilitating extensible distributed systems optimizations.
PUMA is a declarative constraint solving platform for policy-based routing and channel selection in multi-radio wireless mesh networks. We have developed a prototype of the PUMA system using the RapidNet declarative networking system deployed on the ORBIT testbed.
The FVR project addresses a long-standing challenge in networking research — bridging the gap between formal theories and actual implementations. We present the FSR (Formally Safe Routing) toolkit, that unifies research in routing algebras with declarative networking to produce provably-correct distributed implementations for inter-domain routing. In addition to the FSR toolkit, the FVR project has also explored the use of theorem proving and rewriting logic techniques to verify routing protcols.
Operators of distributed systems often find themselves needing to answer forensic questions, to perform a variety of managerial tasks. We present NetTrails, a novel provenance-based approach that provides the fundamental functionality required for answering forensic questions — the capability to “explain” the existence (or change) of a distributed system state at a given time in a potentially adversarial environment.
RapidNet is a development toolkit for rapid simulation, implementation and experimentation of network protocols. RapidNet utilizes declarative networking, a declarative, database-inspired extensible infrastructure that uses query languages to specify behavior. The long term goal of RapidNet is to provide a unified platform for rapid prototyping, synthesis, and deployment of new network protocols.
The DS2 project explores a unified declarative platform for specifying, implementing, and analyzing secure extensible distributed systems. Our work is motivated by the proliferation of large-scale network information systems currently deployed for a variety of application domains including network monitoring infrastructures, cloud computing, content distribution networks, and network routing.
SAFEST: Selectable Anonymity for Enabling SAFER Telecommunications
Older Research Projects
- Networked Systems Programming Projects in ns-3
- A3: Application Aware Anonymity
- MOSAIC: Declarative Platform for Dynamic Overlay Composition
- OntoNet: Scalable Knowledge-based Middleware for Networked Systems
- Veracity: Fully-decentralized Secure Coordinate Systems