<scp>Spectre</scp> : Automated Aliasing Specification Generation for Library APIs with Fuzzing

Static program analysis of real-world software that integrates numerous library Application Programming Interfaces (APIs) faces significant challenges due to inaccessible or highly complex source code. A common workaround is to use specifications that summarize the key behaviors of these APIs for analysis. However, manually writing specifications is labor-intensive and requires a deep understanding of API semantics, while existing automated specification generation techniques struggle when source code is inaccessible or partially available. This article introduces Spectre , an automated framework that leverages fuzzing techniques to generate aliasing specifications for library APIs. Spectre operates efficiently and precisely both with and without source code access. When source code is unavailable, Spectre integrates alias-check observers into the driver program after the API call site and performs black-box fuzzing to explore different API behaviors. If a check is satisfied, the corresponding aliasing specification is generated. When source code is available, Spectre incorporates new grey-box fuzzing features specifically tailored for aliasing specification inference, further enhancing its ability to generate aliasing specifications. We conducted extensive experiments to evaluate the performance of Spectre . Without source code access, Spectre demonstrated its specification generation capability across both Musl, a lightweight C standard library, and eight C third-party libraries. For Musl, Spectre recovered 96.7% of correct manually written specifications and identified 40.0% more aliasing specifications than those written by external experts. For C third-party libraries, all Spectre -generated aliasing specifications were validated as correct through static analysis of the API source code. Spectre is also more complete than other specification inference tools, generating 16.7% more correct specifications for third-party libraries. The practicality of the generated specifications was confirmed, as they improved aliasing analysis in static pointer analysis of client code while maintaining a balance between accuracy and efficiency. The effectiveness of the tailored grey-box fuzzing features was demonstrated by Spectre , identifying 20% more specifications compared to when these features were disabled. These results show that Spectre is an effective tool for inferring aliasing specifications and facilitating static analysis.