1. 7

  2. 4

    It’s always interesting to read these from my field’s perspective. Two things jump out for me: network stack issue; hypervisor. The network stack was said to have lots of layers calling into each other. Requirements of Orange Book for high-assurace certification (even medium-high) required strict, hierarchical layering of system with no looping calls. The computations flowed up with the calls and results strictly going down. Each layer must be proven correct in isolation then each interaction through interface checks & careful analysis. Used abstract, state machines w/ formal proof or some such analysis converted into interacting FSM’s of straight-forward code. It’s why they never had these problems. For idea of what that looks like, see legendary Paul Karger pull it off for his VAX security kernel that virtualized Ultrix and VMS in the 1990’s:


    Note: Many things come from the time and requirements. The design/assurance stuff are the meat that lasts. That’s p8 in “Layered Design” and p12 in “assurance activities.” The layering technique was invented and deployed by Dijkstra for “THE Multiprogramming System.” It was extremely reliable. Many assurance activities, including compiler concerns, have tool support today. Even Microsoft develops and uses them.

    For the hypervisor, might be worth taking a look at one of the modern, high-assurance VMM’s to see if any techniques are worth copying. NOVA microhypervisor gets TCB size down to 36,000 lines of code (9,000 kernel). I imagine clever techniques like that plus OpenBSD folks coding skill and real-world experience might make better VM.


    1. 2

      stsp continues his five year mission to fix wifi. In last week’s episode, he negotiates with the standard violating APs at 33C3.

      Is there a link to the talk? I couldn’t find it on in the Fahrplan.

      1. 6

        It wasn’t a talk, he just noticed the bug and fixed it while he was attending 33c3.

        1. 5

          Yep. Though it’s not a 33C3 talk but a change that makes OpenBSD work better with routers there. Here is the mailing list thread.