I don’t have much to add. Just wanted to say hi and say that my AI security strategy routes mostly through secure program synthesis (which I sometimes abbreviate as SPS), but I’m focused on formal verification. And the fact that it appears 12 CVEs in OpenSSL (i.e., probably the coolest thing going on in SPS right now) happened without a single formal method[1] feels like it should make me drastically alter my plans.
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 :) )
I don’t have much to add. Just wanted to say hi and say that my AI security strategy routes mostly through secure program synthesis (which I sometimes abbreviate as SPS), but I’m focused on formal verification. And the fact that it appears 12 CVEs in OpenSSL (i.e., probably the coolest thing going on in SPS right now) happened without a single formal method [1] feels like it should make me drastically alter my plans.
i don’t know for sure that there is zero “formal methods” in the pipeline, but it seems that way from what’s been said.
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 :) )