| 摘要 |
The invention concerns formal verification and optimization of a program, typically of a virtual machine, initially written in high-level language and implanted for example in a smart card. During verification, it is formally proved (E4) that checks on program states explored by security mechanisms guarantee that a specific forbidden state defined in a high-level language is unreachable by the program. The implantation of the program is then optimised in particular by eliminating execution paths leading to the forbidden state in the program, so as to transform it into a program in a low-level language providing the same security guarantees as the high-level language program. |
