By: Tuba Yavuz (University of Florida) and Ken (Yihang) Bai (University of Florida)
Stage: Software Design and Development
Summary
PROMPT performs component-level analysis using API model guided symbolic execution. API models can be specified using the PROSE API modeling language. PROMPT has been applied to a variety of system code, including device drivers and protocol stack implementations in the Linux kernel and cryptographic libraries.
Contact
Input/Output Interface
- Input: LLVM bitcode and the API model
- Output: A set of test cases and/or reports of various errors
Dependencies
LLVM 3.8
Licensing Info
Apache 2.0
References
Analyzing system software components using API model guided symbolic execution Journal Article
In: Automated Software Engineering, 2020, ISSN: 1573-7535.
Acknowledgments
- Partially funded by by the National Science Foundation awards CNS-1815883 and CNS-1942235 and by the Semiconductor Research Corporation
Additional Information
- A tutorial was presented at IEEE SecDev 2020 (https://secdev.ieee.org/2020/Home) on September 28th 2020