Sử dụng Formal cho bảo mật RISC-V

Finding and closing up security holes is becoming more important as chips are used in safety- and mission-critical applications, but it’s increasingly important for chips designed for much less costly devices, where the selling price typically doesn’t warrant a significant investment in security. The problem is these devices are connected to some of the same networks, and any access points for hackers can compromise a much larger system. This has been a particular concern for RISC-V chips, in which the source code for the instruction set architecture can be modified by the user. Ashish Darbari, CEO of Axiomise, explains how formal verification can be in collaboration with the new Capability Hardware Enhanced RISC Instruction for Internet of Things (CHERIoT), how microarchitectures can compromise entire systems, and why custom instructions in RISC-V make security more difficult.