- Flowlog, a tierless programming language for software-defined networks.
Read more about Flowlog in our papers below, or in our
blog posts (click here) on the topic.
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
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
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
Aluminum is available for download here.
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)
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)