CAV'24 Artifacts paper4986

We propose StarFuzz, that allows F* ineractive theorem prover to provide better end-to-end assurance on the application— even when interfaced with the closed-box components. Verified code extracted from F* interface with external libraries containing real-life complexities—proprietary library calls, remote/cloud APIs, complex models like ML models, inline assembly, highly non-linear arithmetic, vector instructions etc. We refer to such functions/operations as closed-box components. These closed-box components are handled with the user assuming relevant lemmas about them. However, these assumed lemmas may be inconsistent due to (i) incorrect assumed specification and (ii) faulty implementation of closed-box components. To validate consistency of specification and implementation of such closed-box components, StarFuzz constructs a relevant verification condition including the closed-box components, and uses Sādhak under the hood to validate it. In our experiment, we have used StarFuzz to validate around 56 F* specifications used in many library calls that are used in F* proofs. In our collected benchmarks from F* repository, StarFuzz discovered four bugs—one bug that revealed an error on the assumed lemmas for a closed-box function, and three bugs in the external implementations of these components.