«We employed the K framework [59] (Section 2.1) as our formalism medium to leverage its capability of deriving various correct-by-construction formal analysis tools directly from the language semantics. We took Heule et al. [37]’s semantics (Section 2.2) as our starting point to avoid duplicating the formalization effort. We made several corrections or improvements to this semantics, to improve both soundness and efficiency. We automatically translated their semantics into K, and cross-checked the translated semantics against the original using an SMT solver. We manually specified the semantics of the remaining instructions faithfully consulting the Intel manual [11] to obtain the complete semantics. A manual specification may sound like a daunting effort at first, but the fact that (1) x86-64
is largely stable and changes slowly over time, and (2) the state-of-the-art synthesis techniques for language semantics (notably, Strata [37] and Hasabnis et al. [35, 36]) suffer from scalability and/or faithfulness issues (see Section 3.2 and 7 for details), makes the effort worth undertaking.»

«We then translated these SMT formulas from Strata into K rules using a script, and tested the resulting rules by comparing with the Strata rules using Z3.»

Почему мы не можем так же? Другой уровень. У нас ни пруверов (Z3 это прувер), ни солверов, ни фреймворка нет.

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