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.
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.