This repository hosts a modified version of tpm2-tss 2.1.0 that can pass memory safety formal verification. We utilized Abstract Interpretation and the tool TrustInSoft Analyzer to achieve this goal. The original TSS readme is renamed to Original_README.md.
It took us 9 person-months to verify the overall 1300+ funcitons (or 67K+ lines of code). During the verification, We found several potential memory safety flaws (e.g. null pointer dereference, memory leakage, buffer over-read, integer overflow etc.), and made 140+ patches to address them. Under our constraints, the program has been proven to be memory safe. Hopefully this effort can help developers to build memory safe TPM applications, and further contributions from you are always welcome!
Our formal verification process makes no changes to the original building or testing procedures, so please check the original instructions for detailed information.
Please check the original instructions for detailed information.
The verification result is summarized in tpm2-tss-verify-results.md. Each function in this file is followed by its verification coverage, false/true positive counts, whether it’s passed or not, and whether it’s patched by us in order to pass the verification.
The following are some examples. Please check tpm2-tss-verify-results.md for the full result.
| Function Name | Coverage | # of False Positive | # of True Positive | Patched or Not |
|---|---|---|---|---|
| Tss2_MU_TPMS_ALG_PROPERTY_Marshal | 100% | 1 | 0 | No |
| Tss2_MU_TPMS_ALG_PROPERTY_Unmarshal | 100% | 1 | 0 | No |
| Tss2_MU_TPMS_CAPABILITY_DATA_Marshal | 100% | 0 | 0 | No |
| Tss2_MU_TPMS_CAPABILITY_DATA_Unmarshal | 100% | 0 | 0 | No |
| Tss2_MU_TPMS_TIME_INFO_Unmarshal | 100% | 0 | 0 | No |
- Potential memory leaking in iesys_nv_get_name
- Uninitialized variable is referenced in Esys_Quote
- memory leak in iesys_cryptossl_pk_encrypt
- Incorrect SAFE_FREE(name) in Esys_TR_GetName
- Incorrect stop condition for the for loop in iesys_compute_hmac
- Incorrect null check for esys_context in Esys_TR_FromTPMPublic_Finish
Contrbutions are welcome. This modified version is based on tpm2-tss 2.1.0. We are happy if you're interested in verifying the functions newly added in newer releases. Feel free to send us pull requests on the GitHub and join the verification journey with us. If you have questions, you can also talk to our maintainers for help.
Feel free to submit Github issues, pull requests, or contact the following maintainers.