4 ms·
This is really interesting stuff, thanks. I've assumed that without source annotation, the only things that you can verify statically are violations of the run
by lallysingh 7y ago
This is really interesting stuff, thanks. I've assumed that without source annotation, the only things that you can verify statically are violations of the runtime model (e.g., stack overflow, heap corruption). Mostly through inferences on possible value sets of function arguments and return values.
I'm going to have a look at your links more. I guess the question I don't have answered quite yet is how to tell the tool what to look for beyond the language semantics.
- nickpsecurity 7y agoWhat you've assumed is mostly correct. Almost all the annotation-free tools look for violations like you described since that's what most people want. The correctness-oriented work starts with annotated code. The only other thing I know that works without annotations, but sort of similar, is creating the specs from example inputs and outputs. Then, the code can be analyzed against them. What pro's often do, though, is prove the algorithm itself in a higher-level form that captures its intrinsic details, create an equivalent form in lower-level code, and prove the equivalence. That lets you deal with the fundamentals first. Then address whatever added complexity comes in from lower-level details and language semantics.