3 ms·

Checked c is interesting, but I think a more fruitful avenue would be verifast[0]. Verifast is completely compatible with existing c codebases (so you can keep

Checked c is interesting, but I think a more fruitful avenue would be verifast[0]. Verifast is completely compatible with existing c codebases (so you can keep using your existing c compiler), and is able to verify more interesting behaviour than checked c. [1] finds that it would have prevented 5 of 50 recent CVEs in FreeBSD, whose causes include unlocked memory accesses, resource leaks, and bad reference counts. 0. https://github.com/verifast/verifast https://github.com/verifast/verifast 1. https://metasepi.org/en/posts/2020-10-14-avoid-freebsd-security-issue.html https://metasepi.org/en/posts/2020-10-14-avoid-freebsd-secur...

tyingq 6y ago
It mentions "symbolic execution" of code. Does that work fine with kernel code, being that the tool itself isn't in the right ring, etc?
- wahern 6y ago
  Symbolic execution happens before deployment, and often can be incorporated into the compilation pipeline, much like a classic static analyzer. One of the most popular implementations (at least in the FOSS community) is KLEE: https://klee.github.io/ https://klee.github.io/
  - remexre 6y ago
    I think the question being asked includes, "would existing symbolic execution tools be able to tell that e.g. a page-table was mangled"
    - wahern 6y ago
      Symbolic execution would tell you whether a page-table could be mangled, and if so which range of input of values would lead to that state. (Though you may need to annotate your code to define what a bad state looks like if it's not something as simple as a NULL pointer dereference.) But the capacity for achieving that is a function of the engine and how it integrates with the language. Similar to formal verification it's strongly computationally bound in practice, so the best results (e.g. more comprehensive coverage) are achieved when you structure your code in a way that components (functions, groups of functions, etc) can be symbolically executed individually; and when you can drop annotations in the code to narrow down value ranges that the engine can't determine itself within a reasonable amount of time. So in principle a symbolic execution engine could determine whether a page-table could be mangled, but in practice it probably wouldn't be able to definitively tell you one way or another if you simply tossed the entire FreeBSD kernel source code at such an engine. I'm not particularly knowledgable in this space. I'm abstaining from giving a proper description of what symbolic execution actually is because I'll probably just confuse things. But I have used KLEE and even found bugs using it. It's a steep learning curve so once you get to the point where you can make use of KLEE much of the theory will begin to make sense even if you can't describe it properly ;) And if you've ever used formal verification systems, especially ones with strong language integration, things will make sense much earlier. I don't think there's a clean dividing line between symbolic execution and static analyzers. Some modern static analysis tests and optimizations in GCC and clang could be described as employing symbolic execution. A proper symbolic execution engine can just perform such tests more comprehensively, exploring much longer, deeper control flow paths with far greater state spaces.
  - rurban 6y ago
    KLEE is only popular with the HN crowd, but not certainly not in the industry. There cbmc/satabs is leading. Esp. automotive. Also much older, and much easier to use. I recently even added formal verification to my CTL library variant, the STL for C. https://github.com/rurban/ctl/commit/cc65e82ba1fdafcf9c83697a6bb29b9c9291098e https://github.com/rurban/ctl/commit/cc65e82ba1fdafcf9c83697... cbmc found some huge bugs the testsuites were not able to find. KLEE has similar status as Z3. Hugely popular, but rarely used in practice. Educational toys, or used in side-projects only.
anonymousDan 6y ago
For a monolithic kernel? No chance it will be able to give the same security guarantees. Never mind the usual practical issues with symbolic execution like modeling the environment.

tyingq 6y ago

It mentions "symbolic execution" of code. Does that work fine with kernel code, being that the tool itself isn't in the right ring, etc?

wahern 6y ago
Symbolic execution happens before deployment, and often can be incorporated into the compilation pipeline, much like a classic static analyzer. One of the most popular implementations (at least in the FOSS community) is KLEE: https://klee.github.io/ https://klee.github.io/
- remexre 6y ago
  I think the question being asked includes, "would existing symbolic execution tools be able to tell that e.g. a page-table was mangled"
  - wahern 6y ago
    Symbolic execution would tell you whether a page-table could be mangled, and if so which range of input of values would lead to that state. (Though you may need to annotate your code to define what a bad state looks like if it's not something as simple as a NULL pointer dereference.) But the capacity for achieving that is a function of the engine and how it integrates with the language. Similar to formal verification it's strongly computationally bound in practice, so the best results (e.g. more comprehensive coverage) are achieved when you structure your code in a way that components (functions, groups of functions, etc) can be symbolically executed individually; and when you can drop annotations in the code to narrow down value ranges that the engine can't determine itself within a reasonable amount of time. So in principle a symbolic execution engine could determine whether a page-table could be mangled, but in practice it probably wouldn't be able to definitively tell you one way or another if you simply tossed the entire FreeBSD kernel source code at such an engine. I'm not particularly knowledgable in this space. I'm abstaining from giving a proper description of what symbolic execution actually is because I'll probably just confuse things. But I have used KLEE and even found bugs using it. It's a steep learning curve so once you get to the point where you can make use of KLEE much of the theory will begin to make sense even if you can't describe it properly ;) And if you've ever used formal verification systems, especially ones with strong language integration, things will make sense much earlier. I don't think there's a clean dividing line between symbolic execution and static analyzers. Some modern static analysis tests and optimizations in GCC and clang could be described as employing symbolic execution. A proper symbolic execution engine can just perform such tests more comprehensively, exploring much longer, deeper control flow paths with far greater state spaces.
- rurban 6y ago
  KLEE is only popular with the HN crowd, but not certainly not in the industry. There cbmc/satabs is leading. Esp. automotive. Also much older, and much easier to use. I recently even added formal verification to my CTL library variant, the STL for C. https://github.com/rurban/ctl/commit/cc65e82ba1fdafcf9c83697a6bb29b9c9291098e https://github.com/rurban/ctl/commit/cc65e82ba1fdafcf9c83697... cbmc found some huge bugs the testsuites were not able to find. KLEE has similar status as Z3. Hugely popular, but rarely used in practice. Educational toys, or used in side-projects only.

anonymousDan 6y ago

For a monolithic kernel? No chance it will be able to give the same security guarantees. Never mind the usual practical issues with symbolic execution like modeling the environment.