Re:Memory Model Verification at the Trisection of Software, ...
by gumby on Friday October 26, 2018 @09:14PM
(#18313831)
That's a good question -- I should not have been so terse/flip. I agree they do find some interesting issues and that's why I liked the paper.
On the practicality side: If I read the paper correctly this is a lint like tool for finding suspected problems (hence e.g. the "litmus tests" -- the tool iterates out the possible states, which is great). It isn't a tool for finding new problems. The compiler testing is interesting (I'm an former compiler guy) but reading Sec 7 didn't lead me to believe it could identify code generation problems in cases of very high optimizations.
Also a lot of recent security issues have been in the implementation of the microarchitecture (not just microcode bugs but functional unit errors such as the recent hyper threading leaks).
On the practicality side: If I read the paper correctly this is a lint like tool for finding suspected problems (hence e.g. the "litmus tests" -- the tool iterates out the possible states, which is great). It isn't a tool for finding new problems. The compiler testing is interesting (I'm an former compiler guy) but reading Sec 7 didn't lead me to believe it could identify code generation problems in cases of very high optimizations.
Also a lot of recent security issues have been in the implementation of the microarchitecture (not just microcode bugs but functional unit errors such as the recent hyper threading leaks).
Maybe I am being too harsh?