https://github.com/linux-test-project/ltp is useful for bootstrapping Gnu/Linux kernel verification.
https://sourceware.org/glibc/wiki/Testing/TestsuiteNot for bootstrapping Gnu C standard library verification. Is there an LLVM option to wipe registers before/after function calls; or fence a function to a small set of memory reads/write addresses? Easier to reason with a small side effect surface. The Haskell/Ocaml linker metadata practices need to be brought into LLVM. If foo() makes a write() call to the operating system it needs to be documented as IO in linker metadata. Right now I am doing a whole program LLVM IR representation and inspecting the call graph. On Thu, Jan 19, 2017 at 1:04 AM, Chris Palmer <snackypa...@gmail.com> wrote: > The state of the art is well below the state of the art. :) That is, there > are many problems for which we know decent or even good solutions, and have > known of them for a long time, but for social, political, economic, > interpersonal, or personal reasons, we can't adopt the solutions. (I've > talked about examples in various blog posts and talks and stuff.) > > So I don't spend much time thinking about formal methods, post-quantum > crypto, and other such fancy things. (I'm too dumb to understand that stuff > anyway.) First let's use what type systems/crypto/OS primitives/et c. we > already have. Basic stuff. I have a feeling that the craving for fancy magic > would lessen if we could get the basics nailed down. > > By the time we finally nail down the basics, some of the fancy magic will > have materialized, as it has been gradually doing all along. (Compare the > evolution of type systems in practical languages from BCPL to Rust; or the > evolution from old-timey lint to a modern day clang with all the warnings > turned on; or from the first fuzzer to modern ASan/TSan/UBSan. We actually > have delightfully fancy stuff! Now go use it! :) ) > > And of course, the most effective technique at our disposal is sheer > white-knuckled simplicity. Although that's the one we have the least hope of > applying, it should always be the first one we try. > > _______________________________________________ > langsec-discuss mailing list > langsec-discuss@mail.langsec.org > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > _______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
