Из работы 2017-06-08, Dasgupta, A Complete Formal Semantics of x86-64

«Existing Semantics for x86-64 To date, to the best of our knowledge, despite several explicit attempts [32, 33, 37] and other related systems [13, 35, 36, 41, 42], no complete formal semantics of x86-64 exists that can be used for formal reasoning about x86 binary programs. Heule et al. [37] presented a formal semantics of x86-64, but it covers only a fragment (∼47%) of all instructions; as the authors of [37] candidly admitted, their synthesis methodology proved insufficient to add the remaining instructions primarily due to limitations of the underlying synthesis engine. Moreover, their semantics misses certain essential details (Section 3.6 & 4).
Goel et al. [32, 33], on the other hand, specified a formal semantics in the ACL2 proof assistant [38], allowing to reason about functional correctness, but their semantics covers only a small fragment (∼33%) of all user-level instructions.
There also have been several attempts [20, 24, 35, 60] to indirectly describe the x86-64 semantics, where they define an intermediate language (IL), specify the IL semantics, and translate x86-64 to the IL. This indirect semantics, however, may not be general enough to be used for different types of formal analyses, since the IL might be designed with specific purposes in mind, not to mention that the translation may miss certain important details of the instruction behaviors.
Refer to Section 7 for a more detailed comparison to existing semantics.»

Отредактировано Лис (2024-08-24 04:40:43)