1. 12
  1.  

  2. 5

    Summary:

    “Out of the twelve functions analysed, seven of them were fully proven and the rest had few missing proof obligations: two functions had one, one function had two and two functions had more. In total, 1208 proof obligations were automatically generated including 241 safety verification conditions that cover memory and integer safety. 1194 of these were proven and only 14 which constitute 1.2% of the total number were not proven.

    No issues were detected in the code which is not surprising given the safety and reliability record of OpenBSD despite the pitfalls of C language in terms of security issues. Some minor issues and areas that possibly needed more clarification were highlighted for the documentation.”

    1. 1

      That’s actually why I didn’t save or submit the paper back when I found it. It’s still interesting. I just thought author picked bad functions to verify given they’re highly-used, simple, and would contain the errors OpenBSD devs are good at finding. I figured they found all the bugs in it already. Conclusion confirmed that.

      Best route for using formal methods on a project like OpenBSD is to first determine which kind of bugs they’re knocking out regularly vs getting hit with often. They’re good at mitigating and finding the mistakes that would’ve happened in the string operations, esp like overflows. They keep having NULL dereferences, use-after-frees, and so on. Temporal errors. Using or developing techniques for finding those will help them out a lot.

      If looking for stuff like overflows, best to aim the formal methods at new code that just came in. It will have had less review. Preferably in something critical like filesystem, network stack, or VMM. The new VMM really needs anything people can throw at it since it does a tough job of containing potential malice or just out-of-control VM’s.

      1. 3

        I just thought author picked bad functions to verify given they’re highly-used, simple,

        Well try finding functions with the following requirements:

        The following were the unsupported C features of the Jessie plug-in at the time of the writing [24]:

        • Arbitrary gotos. Some simpler forward gotos are allowed.
        • Function pointers.
        • Arbitrary casts. There was some experimental support for casting between pointers (except in specifications).
        • Union types.
        • Variadic functions.
        • Floating point computations.

        The list definitely got smaller for software verification since then. But sadly it is still there.

        My bachelors thesis is about finding already known bugs (the erratas) with CPAchecker in OpenBSD. And a lot of effort went into making the tool understand the OpenBSD quirks until I didn’t have enough time anymore. Only three more weeks! If something useful comes together I will post it on lobsters.

        1. 1

          It’s tricky. The first rule of high-assurance projects in the past was doing your formal specs and algorithms in easiest-to-verify way. The technique I’d use is rewriting the code to use easier-to-analyze constructs with equivalence check and/or tests. Then, apply the verification tools. If problems are found, inspect the original code to be sure they had them. Floating-point is an exception to this but there’s tools for handling it coming online. There’s a lot of R&D in that right now for both automated and manual proofs. One paper also had a type system for safe casts, too, where you only verify the risky ones.

          “My bachelors thesis is about finding already known bugs (the erratas) with CPAchecker in OpenBSD.”

          Interesting. That’s a good way to empirically verify or reject the claimed effectiveness of the tools, too. On top of showing them where they need to improve on it. Good luck. I look forward to reading it when you post it here. :)

        2. 2

          Best route for using formal methods on a project like OpenBSD is to first determine which kind of bugs they’re knocking out regularly vs getting hit with often.

          Some time ago I aggregated bugs from OpenBSD errata to a single table with bug classes. Perhaps it would be useful for you.

          If looking for stuff like overflows, best to aim the formal methods at new code that just came in.

          Formal verification is a complex and time consuming task. Using it for a new code can be a waste of time. AFAIK the most popular practice is stabilizing functionality with testing and then then applying formal methods.

          1. 1

            re table. Thanks. Bookmarked it.

            re verification. You caught me slipping since that’s normally my advice. I should’ve clarified by new that I meant “newer” code that just hasn’t been in the kernel long. How new varies with effort required. So, static analysis with low, false positives should be aimed at all code in the repo that passed functionality tests. Stuff involving writing contracts could go into new stuff that shouldn’t change really fast. Full, formal verification should only be done on stuff that’s critical and staying for a long while.

            That distinction is also why I push for memory-safe languages with contracts. There’s hardly any effort upfront to keep it secure. Rust’s borrow checker might be an exception. They report it gets easier after a learning curve. Contracts can be as simple as ranges to at least stop overflows and test boundary conditions better. In any case, using better tools than C also helps. I’m not going to try selling them on that yet.

      2. 2

        Note that this was based upon OpenBSD 4.6.