This technology is a multi-model approach to verify the security of modern computing systems with relaxed memory behavior.
Modern computer systems often use relaxed memory behavior and reorder certain memory operations within constraints defined by instruction set architecture (ISA). However, these current methods for security verification use sequentially consistent models which depend on strict ordering rules. These approaches do not properly account for relaxed memory behavior which leads to weak security and failure to account for subtle threats to modern hardware.
This system verification application uses a multi-model approach to address relaxed memory behavior of modern computing systems. This technology decomposes the system into a smaller core and a larger set of services, enabling it to verify each core and its properties, and propagate the guarantees to the entire system. This approach is compatible with existing verification techniques and can be applied to modern computing for improved protection and security verification.
IR CU21004, CU19395
Licensing Contact: Greg Maskel