Selected Research Translation & Impact

Our research extends beyond fundamental technical advances to address challenges with direct societal, industrial, and governmental relevance. The work highlighted below demonstrates how RISING Lab research contributes to safer and more reliable computing systems, supports emerging technologies and critical infrastructure, and helps translate academic innovation into practical impact.

Formal Verification of High-Assurance Machine Code

Co-developed a novel approach to verification condition generation via theorem proving and compositional cutpoint reasoning that enabled scalable, compositional verification of machine-level programs directly over operational machine models. The methodology catalyzed independent research and application across multiple organizations: it was used at Galois Connections for binary code verification on Rockwell Collins AAMP7™, at the National Security Agency for assembly language verification on the Mostek 6502, at Rockwell Collins for AAMP7 and JVM code verification, and in subsequent verification infrastructures at Stanford University and the University of Cambridge. The work also contributed directly to DARPA’s Secure, High-Assurance Development Environment (SHADE) program, including machine-code verification for highly secure AAMP7 applications. Ray subsequently served as Principal Investigator at the inception of the DARPA CRASH project on Code Verification for Practical Machine Architectures, extending such verification toward realistic software and processor architectures.

Formal Verification of Industrial Memory Designs

Developed refinement-based abstractions and mechanized verification methods for custom and non-volatile memories whose analog and specialized transistor behavior prevents conventional digital verification abstractions from being applied directly. In collaboration with Freescale Semiconductor Inc., the methods were applied to industrial flash memory implementations based on both floating-gate and split-gate technologies, producing the first reported formal functional verification results for industrial flash memories. The foundational custom memory verification work received a Best Paper nomination at FMCAD 2007.

Certified Behavioral Synthesis

Developed a tool-independent formal certification framework combining theorem proving and automated sequential equivalence checking to establish that RTL generated through behavioral and high-level synthesis preserves its source-level specification. The framework addressed compiler transformations, scheduling, resource allocation, implementation optimizations, and loop and function pipelining, and scaled to industrial-size designs with more than 32,000 lines of generated RTL. The methods were evaluated extensively on designs generated by commercial synthesis technology, including AutoESL, and exposed correctness errors in synthesized hardware; one published study reported the discovery of a previously unknown bug in a commercial synthesis tool. The resulting ForSyn technology was presented through a series of technical reviews and interactive demonstrations to Intel. The project was selected and reported by NSF as a research highlight in 2010.

Post-Silicon Validation and Debug

Developed systematic methods for post-silicon observability, trace-signal selection, limited-observability trace analysis, protocol reconstruction, and application-level hardware tracing. The research addressed industrial validation problems through work and collaborations involving researchers from Intel, NXP, IBM, and academic partners. Application-level tracing was demonstrated on the industrial-scale OpenSPARC T2 processor at a scale beyond the capability of prior tracing approaches, achieving 98.96% trace-buffer utilization and 94.3% average flow-specification coverage while reducing potential root causes to 21.11% on average. Publications from this research received Best Paper nominations at ICCAD 2015 and DAC 2018, and related contributions received multiple Intel research recognition awards specifically recognizing their impact on Intel products and tools.

Secure System-on-Chip Architecture and Validation

Developed policy-driven architectures and validation methods for enforcing system-level security requirements in Systems-on-Chip containing heterogeneous or potentially untrusted components. The work introduced configurable security infrastructure and wrappers, runtime policy enforcement, formal security-policy validation, hardware patching, secure provisioning, and protection of on-chip communication fabrics. The vision of configurable and evolvable SoC security was also articulated publicly in a 2017 IEEE Spectrum feature on patchable hardware. This body of collaborative research provided significant technical motivation for DARPA’s subsequent four-year, $75M Automatic Implementation of Secure Silicon (AISS) program, which sought to automate the integration of scalable security mechanisms into SoC designs with differing security, performance, and cost requirements. The research subsequently formed the foundation for the team’s Security Engine and Core Platform contributions under AISS and has also contributed to issued patents covering runtime security protection, trusted IC provisioning, and related secure-system technologies.

Automotive Security and Resilience

Developed systematic methods for security assurance of connected and autonomous vehicles, spanning attacks on vehicular sensing and communication, resilient control, automated security evaluation, and virtual and digital twin platforms for safety and security exploration. The work introduced RACCON, the first framework providing real-time resiliency for a cooperative automotive application, enabling vehicles to detect and mitigate malicious communications during operation rather than merely identify attacks. Subsequent research developed extensible infrastructures for automated security evaluation and digital-twin environments for exploring interactions among automotive electronics, safety failures, and cyberattacks, and extended the analysis to emerging sensing and control architectures including steer-by-wire systems.