i don’t know for sure that there is zero “formal methods” in the pipeline
in discovering the 12 OpenSSL zero-day vulnerabilities, we haven’t used any formal methods. since then, we incorporated some. the (discovery --> CVE assigned --> CVE made public) pipeline is a very lagging indicator and the OpenSSL results are reflective of the state of the AISLE system approximately mid-fall 2025, prior to our use of formal methods
Hi Stanislav, can you expand on what you mean when you say you’re using FM? I.e., are you referring to symbolic analysis / concolic analysis techniques, model checking, formal methods in the sense that you dispatch a question of “go right or go left?” to z3, formal methods in the sense of grammar-based fuzzing or property based testing (lightweight FM), or do you mean you’re doing full-blown theorem proving (I don’t exactly see why you would be doing this but I’m open to being told I’m wrong :) )
in discovering the 12 OpenSSL zero-day vulnerabilities, we haven’t used any formal methods. since then, we incorporated some. the (discovery --> CVE assigned --> CVE made public) pipeline is a very lagging indicator and the OpenSSL results are reflective of the state of the AISLE system approximately mid-fall 2025, prior to our use of formal methods
Hi Stanislav, can you expand on what you mean when you say you’re using FM? I.e., are you referring to symbolic analysis / concolic analysis techniques, model checking, formal methods in the sense that you dispatch a question of “go right or go left?” to z3, formal methods in the sense of grammar-based fuzzing or property based testing (lightweight FM), or do you mean you’re doing full-blown theorem proving (I don’t exactly see why you would be doing this but I’m open to being told I’m wrong :) )