My interest was piqued by a question on the questions-and-answers site Quora (the irritating one that tries to get you to register by limiting the number of answers you can view in a month otherwise; no, now you’re thinking of Medium; I mean the one that was doing this from the beginning). The question was about the differences between the B method and Frama-C. The existing answer at the time was making some good points, but I thought the phrase “First you are supposed to write or find some C source codes” in the existing answer was backwards. So I wrote my own answer there.
Why Exhaustive Static Analysis is the key to validating a secure and reliable Trusted Execution Environment
In Part 1 of this series, we discussed why the code of a trusted execution environment (TEE) needs to be completely free of undefined behaviors (bugs) and why