Microverification security of modern computing systems with relaxed memory behavior

This technology is a multi-model approach to verify the security of modern computing systems with relaxed memory behavior.

Unmet Need: Security verification approaches do not account for 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.

The Technology: Extended microverification process to modern computing systems with relaxed memory behavior

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.

Applications:

  • Hardware protection for government agency systems
  • Microprocessor hardware protection
  • Hardware memory protection
  • Cell phone and personal equipment hardware protection
  • Videogame console hardware protection
  • Open source adoption by Linux community

Advantages:

  • Improves protection and security verification for modern computing systems
  • Extends microverification process to relaxed memory hardware
  • Can overcome the challenges of highly parallelized and heterogenous systems
  • Verifies programs with less proof burden

Lead Inventor:

Jason Nieh, Ph.D.

Related Publications:

Tech Ventures Reference: