BU/MIT Lincoln Lab Collaboration
The Hariri Institute for Computing and MIT Lincoln Laboratory (MIT LL) have a multi-faceted research collaboration that brings together BU faculty and students with MIT Lincoln Lab technical leaders. Research topics of interest include verifiable security models, security as a service, moving target defense, secure cloud computing and others.
Why We Need This Collaboration
Next generation cyber-physical systems (CPS) are expected to be deployed in domains which require scalability as well as performance under dynamic conditions. This scale and dynamically will require that CPS communication networks be programmatic (i.e., not requiring manual intervention at any stage), but still maintain iron-clad safety guarantees.
Software-defined networking standards like OpenFlow provide a means for scalable building tailor-made network architectures, but there is no guarantee that these systems are safe, correct, or secure. A system design strategy based on the complementary pairing of software-defined networking and formal modeling and verification may enable the CPS community to build next-generation systems without sacrificing the safety and reliability that these systems must deliver.
What We Hope To Achieve
The goals of this initiative are to develop formalisms and methodologies, as well as accompanying interfaces, languages, and tools, for specifying and modeling distributed systems while taking advantage of existing formal modeling and verification techniques and technologies.
In particular, users within application domains who are not necessarily experts in formal methods themselves should be supported in employing formal methods to analyze critical requirements, invariants, and other properties of systems during the design stage, prior to their implementation.
Some project examples include:
- Apply Verificare to the analysis of real scenarios and establish a community for it.
- Application of formal method techniques in analyzing low-level system behavior (e.g. runtime model checking of assembly to prevent ROP attacks),
- Application of model checking in security metrics and quantitative measures of system behavior
- Evaluation and characteristic modeling of real-world attacks.
What We’re Looking At Right Now
The current focus of research collaborations is Moving Target Defense and the Verificare project.
Verificare is a modeling tool and underlying formalism supporting the rapid, iterative development of modular, composable distributed system specifications, and the automated formal verification of the invariants and properties thereof (chosen by the designer). The tool incorporates a number of translation components in its backend that can convert both system descriptions and formal properties into languages and representations understood by off-the-shelf verification tools such as Alloy and Spin.
How We Share Our Work
BU and MIT LL host Cybersecurity Workshops. The series provides occasional one-day workshops open to the public, each focusing on a specific aspect of cybersecurity. In 2014 we covered Moving Target Defense. Then in 2015 we focused on Secure Cloud Computing and Storage.
These workshops seek to bring together researchers from a diverse array of backgrounds, from industry and academia, in order to report on research findings, opportunities and challenges in the burgeoning field of cybersecurity.
The BU/MIT LL collaboration includes these current and future potential activities:
- Sponsor and co-advise graduate student research.
- Host BU students at MIT LL as interns during summer and/or the school year.
- Apply for joint projects to the funding agencies such as DHS, NSF, DARPA, etc.
- Develop joint seminars and workshops and/or hackathons.
- Define undergraduate course projects for students to get more engaged with research and possibly pursue further in grad-school as appropriate.
This collaboration is led by Institute Visiting Fellows Dr. Hamed Okhravi and Dr. Richard W. Skowyra, Technical Staff, of the Cyber Systems and Technology Group at MIT Lincoln Lab along with Azer Bestavros, Hariri Institute Director and Andrei Lapets, Hariri Associate Director of Research Development.