So, without digging into paper, it basically is about creating many test-cases to assess strengths and weaknesses of static analysis tools that should theoretically have found those injected bugs? As in previous comment, that could be a whole field of research in itself if it's not already. I'm not just talking about common case of injecting to test static analysis. Here's a few that pop into my mind as I run through old Orange Book and EAL lifecycle:
1. Inject flaws into formal specification of problem. Knowledge-based methods might do that for modifications in domain representing slip-ups of experts. Semantic methods might modify specs directly to flip a logical property. Preferably one similar to it to increase odds that they overlook it.
2. Formal policy of safety or security. This is a policy, type system, info flow labels, access control matrix... any of that. The injections would deliberately weaken the policy. This would combine templates that ensure common flaws got represented plus truly random ones. Lean more toward templates here as opponents will want to create things that break policy in catastrophic ways. That likely, but not certainly, means they'll focus on specific areas of policy for mods.
3. Formal verification. Similar to above or code-level tests but for intermediate forms or verification conditions. Maybe for proof tactics too if someone is trying to design a prover that doesn't get lost for too long. I think a simple time-out with trace log would suffice for that, though.
4. Code is the next part. You people largely have it covered in isolation. However, it must map to specs or requirements in high-assurance products. So, the mappings could be screwed up where code is tweaked to mis-match the spec similar to how specs are tweaked above. Also, the Design-by-Contract or other invariants might be modified to mislead an evaluator like SPARK Examiner or Astree Analyzer. If it supports it, the compiler instructions or pragma's might be modified to make compiler inadvertently break the code.
5. Testing. There's already a lot of work on this one where compilers, analyzers, tests, and/or fuzzers are mixed. I'll leave them to it as only basics are really needed for high-assurance. Other benefits or methods are still debated.
6. Effects of optimizations on source to object translation. Starts with equivalence checking ability. From there, different optimizations are used to try to break safety/security/correctness properties of the code with tool attempting detection. Goal of injector is to prevent that. Eventually, a corpus would be generated here of software fragments, transformation, and result that could tell us more via machine learning techniques. That's true of above in general but SSA etc is low level & small.
7. Covert channel analysis. Step most "secure" software misses although mainstream rediscovering it slowly as "side channels." Mainly focus on storage, timing, and resource exhaustion channels. Create tools to find the connections automatically in software either statically or dynamically with a test suite in progress. Inject covert channels all over the place. See what it finds.
8. Type systems. They're usually eyeballed or analyzed with formal methods. Often abstractly. I'd like to see above code- and formal-level injection combined to produce and test possible failures of executable, formal spec of type system and/or implementations of it. I bet it would find something.
So, there's what's off top of my head as I apply my mental framework for high-assurance security onto the abstract of your LAVA tool. Much potential for research and results if this grows into its own field. All I ask if you or one of your PhD's turns this into real papers is credit for contributing the idea to do so. :)
Regardless, what do you think of these? Are other people doing them? Are they novel? Which you see most bang for buck? Far as I can tell & based on current market share, biggest impact in order are static analysis, compiler optimizations, type systems, covert channels to stop memory leaks, and improved formal policies to support type systems and design-by-contract. The rest possibly useful but less so.
Note: The short-cut link on your Twitter to your blog was hilariously named. If it was intentional.