Enable model checking on edk2 with cbmc - shijunjing/cbmc GitHub Wiki

This work is try to enable the Model Checking formal method on edk2 firmware verification.

Useful links and papers:

• Model checking. https://en.wikipedia.org/wiki/Model_checking
• Cook, Byron, et al. "Model checking boot code from AWS data centers." International Conference on Computer Aided Verification. Springer, Cham, 2018. https://rd.springer.com/content/pdf/10.1007%2F978-3-319-96142-2_28.pdf
• CMU course: Bug Catching: Automated Program Verification https://www.cs.cmu.edu/~15414/schedule.html https://www.cs.cmu.edu/~15414/f17/schedule.html
• How CBMC Works: http://www.cs.tau.ac.il/~msagiv/courses/asv/BMC.pdf
• Open-sourcing Facebook Infer: Identify bugs before you ship: https://code.fb.com/developer-tools/open-sourcing-facebook-infer-identify-bugs-before-you-ship/
• Abstract Interpretation in a Nutshell: https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html
• HotOS'19 - RedLeaf : Towards An Operating System for Safe and Verified Firmware: https://dl.acm.org/citation.cfm?id=3321449