11–18 of 18 posts
The only option for windows is manual compilation using a POSIX library. Any suggestions for a similar tool?
What would this say on the OpenSSL code that had the Heartbleed bug? (Edit) this: https://news.ycombinator.com/item?id=7571506
You can look at the Frama-C blog what it does with a major openssl competitor, polarssl. http://blog.frama-c.com/
It is very handy - http://xvilka.me/frama-c.png - screenshot of the integer overflow found.
The only option for windows is manual compilation using a POSIX library. Any suggestions for a similar tool?
Cppcheck - http://cppcheck.sourceforge.net/
I ran it over a couple of old finished projects and it found a problem in each one. Awesome.
Unfortunately it misses a class of errors memcpy would do,( similar to heartbleed ) , if copy size is determined at runtime.
I like Frama-C a lot in theory, though in practice I found it hard to use except on very small code segments. When its unable to prove a range the feedback you get from the solvers is inscrutable enough that its very hard to figure out what additional data it would need to satisfy the analysis. (Sort of like parsing C++ compiler template related errors) I'd hoped that language features like the typestate stuff that u…
> I'd hoped that language features like the typestate stuff that used to be in Rust would someday make the work required to use sound analysis tools in production code smaller. I'm not sure if much thought has been given to what kinds of accommodations languages could give to ease static analysis while still being programmer friendly. Well, since the Rust borrow check is basically a static analysis that's always on a…
Earlier quoted context omitted.
> I'd hoped that language features like the typestate stuff that used to be in Rust would someday make the work required to use sound analysis tools in production code smaller. I'm not sure if much thought has been given to what kinds of accommodations languages could give to ease static analysis while still being programmer friendly. Well, since the Rust borrow check is basically a static analysis that's always on a…
I played with Rust for a day and while I was impressed with the language as a whole, I felt the borrow checker left a lot to be desired. I don't think having lifetime of references tied to scope works well in general. This is most evident in pattern matching where you are forced to grab your reference in the pattern (even if you don't need to use the reference until much further on), and there is no way to release it…
Having a borrow check is important, because otherwise you're left with iterator invalidation and numerous other memory safety holes.
I like Frama-C a lot in theory, though in practice I found it hard to use except on very small code segments. When its unable to prove a range the feedback you get from the solvers is inscrutable enough that its very hard to figure out what additional data it would need to satisfy the analysis. (Sort of like parsing C++ compiler template related errors) I'd hoped that language features like the typestate stuff that u…
> I'd hoped that language features like the typestate stuff that used to be in Rust would someday make the work required to use sound analysis tools in production code smaller. I'm not sure if much thought has been given to what kinds of accommodations languages could give to ease static analysis while still being programmer friendly. Well, since the Rust borrow check is basically a static analysis that's always on a…
If a program does anything important, if it handles secrets, if it enforces invariants ("the robots arm must not be out of the safe area"), etc. then other aspects of the programs logic may be just as safety critical as memory safety. Frama-C can prove other things about program saftey: this calculation cannot overflow, this error state can never be reached, this operation will complete within X steps... even if the results of non-safety don't result in anything to do with memory errors.
Some of the programmers expectations can be extracted from the program— signed integers won't overflow, loops (unless otherwise annotated) will always terminate, pointers will not be extended outside of their objects, a pointer to an integer won't be called as a function pointer, behavior will not depend on the order function arguments are evaluated in, etc. Some of the expectations must be expressed as assertions.
Once as many of the programmers expectations are understood the analysis needs to know the invariants that allow them to be true. Some of these can be extracted, some must be asserted.
The gap that exists today is that a lot that could be extracted (e.g. by another programmer reading in a context free way, with high probability of success) can't be soundly extracted because there is a lot of technically valid behavior which is just usually unlikely to be what anyone intended. This means that anyone attempting to apply tools like frama-c has to spend a lot of time making the implicit assumptions explicit with assertions. Thats why I was saying that something like making singed overflow defined may be a step backwards because it takes a whole class of "you couldn't possibly have intended this behavior" back to "maybe you meant this".
Earlier quoted context omitted.
> I'd hoped that language features like the typestate stuff that used to be in Rust would someday make the work required to use sound analysis tools in production code smaller. I'm not sure if much thought has been given to what kinds of accommodations languages could give to ease static analysis while still being programmer friendly. Well, since the Rust borrow check is basically a static analysis that's always on a…
Right, the borrow checker does great things. But memory safety is only one aspect of program correctness— though a universal and very important one. If a program does anything important, if it handles secrets, if it enforces invariants ("the robots arm must not be out of the safe area"), etc. then other aspects of the programs logic may be just as safety critical as memory safety. Frama-C can prove other things about…