Software
- Flowlog, a tierless programming language for software-defined networks
Download Flowlog here.
- The Margrave Tool for Policy Analysis
Margrave provides concrete scenarios that illustrate how
security policies behave and interact. One might ask Margrave how
packets are handled differently by different paths through a network,
or use it to discover which policy rules contribute to that
difference.
Margrave supports several real-world policy languages, as well as its
own intermediate policy language, and provides a flexible query
language for users interested in verifying properties or in narrowing
the scope of scenarios given.
For more information,
visit The Margrave Project
Homepage
- Aluminum
Aluminum is a modification of
the Alloy Analyzer that
presents only minimal models: those in which every fact is
necessary. Aluminum also lets users explore the scenario space for a
specification by augmenting a given model with consistent facts; the
resulting minimal models illustrate the consequences of such
additions.
Aluminum is available for download here.
Publications
-
Geometric Logic for Policy Analysis
Salman Saghafi, Tim Nelson and Daniel J. Dougherty
International Workshop on Automated Reasoning in Security and Software Verification (ARSEC) 2013
-
Toward a More Complete Alloy
Tim Nelson, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi
3rd International Conference on Abstract State Machines, Alloy, B, and Z (ABZ 2012)
-
The Margrave Tool for Firewall Analysis
Tim Nelson, Christopher Barratt, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi
24th USENIX Large Installation System Administration Conference (LISA 2010)
-
On the Finite Model Property in Order-Sorted Logic
Tim Nelson, Daniel J. Dougherty, Kathi Fisler and Shriram Krishnamurthi
Synthesis, Verification, and Analysis of Rich Models (SVARM 2010)
Technical Reports
Thesis