Vigor
Formally verified and performant software middleboxes
Software stack and toolchain for building and running software middleboxes that are guaranteed to be correct, while providing competitive performance and preserving developer productivity. With Vigor, developers write the middlebox code (i.e., the software network function, or NF) in C atop a standard packet-processing framework, putting persistent state in data structures from a Vigor-provided library. Vigor then automatically verifies that the resulting software stack correctly implements a specification (written in Python).
Network
Key facts
Maturity
Support
C4DT
Lab
Key facts
Maturity
Support
C4DT
Lab
- Technical
- Research papers
- Source code: Project Github
- Last commit: 2021-03-06
The Dependable Systems Lab develops techniques and abstractions for building trustworthy computer systems, i.e., systems that are safe and secure. They:
- Explore the fundamental challenges posed to security and safety by large-scale systems consisting of many threads, many nodes, and millions of lines of code written by many programmers
- Seek solutions that solve real-world problems by overcoming theoretical worst-case limitations
- Build open-source prototypes that enable evaluation of these solutions with real-world workloads
- Operate at the intersection of operating systems, distributed systems, programming languages, formal methods, and computer architecture
This page was last edited on 2022-07-05.
This page was last edited on 2022-07-05.