The increasing complexity of networked computing systems makes modern network systems vulnerable to various attacks against their resources, infrastructure, and operability. While the reasons for such attacks may be tied to complex sociological issues, the cause of our inadequate defense solutions lies in the single-layered approach used to address computer systems security. Current security approaches separate defense strategies into distinct realms, either hardware or software. Accordingly, cross-layer approaches for secure computing and circuit systems are entirely lacking. In addition, the wide usage of third-party IP cores and outsourcing fabrication/packaging services make it possible for malicious hardware modules to enter the design flow and, therefore, complicates the problem of trusted system design and verification. The Security in Silicon Lab (SSL) focuses on these areas and tries to develop solutions address IP core security, cross-layer protection, smart device security, and AI security.
1. IoT/CPS Security Vulnerabilities Database
In order to support the research of IoT and CPS protection, we try to investigate the IoT device security and identify security vulnerabilities of various devices. Based on our work, we are building the first IoT Security Vulnerability Database (IoT-SVD). A few device samples are listed below. Please contact the lab PI at yier.jin@ece.ufl.edu for more details about our work. Requested by device manufacturers, we will not reveal vulnerability details without their permissions.
Courtesy of Manufacturers
2. Hardware IP/SoC Formal Verification
Theorem provers are used to prove or disprove properties of systems expressed as logical statements. Since 1960s, several automated and interactive theorem provers have been developed and used for proving properties of hardware and software systems. Following this trend, we developed a new Proof-Carrying Hardware (PCH) framework, which uses an interactive theorem prover for verifying security properties on IP cores and SoC platforms. In the framework, Hoare-logic style reasoning is used to prove the correctness of the RTL code and implementation was carried out using the Coq proof assistant. As Coq supports automatic proof checking, it can help IP customers to validate proof of security properties with minimum effort. Based on this PCH framework, a new trusted IP acquisition and delivery protocol was proposed, in which IP consumers provided both functional specifications and a set of security properties to IP vendors. IP vendors then developed the HDL code based on the functional specifications. The HDL code and security properties were then translated to calculus of inductive construction (CIC). Subsequently, proofs were constructed for security theorems and the transformed HDL code.
Figure 1. PCH supproted IP transaction framework
3. Security Enhanced Processor Architectures for Cybersecurity
The high complexity of modern computer systems, while helping improve system performance, has also complicated the problem of system security. Therefore, cybersecurity researchers heavily rely on layered security protection approaches and have developed various methods to protect the higher abstract layer through security enhancement at the lower abstract layer. Through this chain, cybersecurity protection schemes have been pushed downward from virtual machine to hypervisor. With cyberattacks being developed to compromise the hypervisor, cybersecurity researchers start to take hardware into consideration. Hardware infrastructures are modified to directly support sophisticated security policies so that system level protection scheme can be more efficient and effective. Upon this request, we have developed security-enhanced processor/microprocessor architectures which can prevent various cyberattacks. The developed hardware infrastructures are of high efficiency to prevent cyberattacks with very low performance overhead. For example, we have proposed hardware solutions to successfully detect malicious loadable kernel modules and ROP attacks on on various architectures including SPARC, x86, etc.
4. Gate-Level Netlist Security Analysis and Protection
Third-party resources in hardware circuit designs, mostly in the format of soft/hard IP cores, are prevailingly used in modern circuit designs alleviating the design workload and shortening the time-to-market (TTM). However, the wide usage of third-party IP cores also breeds security concerns that the delivered IP cores may contain malicious logic and/or design flaws which will be exploited by attackers after the IP cores integrated system is fabricated. With existing tools focus on RTL code security evaluation, we focus on developing automatic netlist analysis tools to validate security properties on netlist and fabricated circuits. Two automated netlist analysis tools, RESim and REFSM, have been developed to help IP users to fully understand the IP core functionality without requesting RTL source code. The RESim is developed based on weakly-affecting node theory and helps reconstruct RT-level descriptions around suspicious nodes. The REFSM is developed under a more general scenario to help IP users to recover the precise RTL code of the FSM within target netlist. The automatically generated output of the REFSM will help IP users to clearly identify the control flow in the delivered IP cores so that malicious states can be detected.
Figure 2. Demo on REFSM in identifying finite state manchines from netlist
5. Emerging Devices in Hardware Security
The development of emerging technologies provides hardware security researchers with opportunities to utilize some of the otherwise unusable properties of emerging technologies in security applications. Originally developed as alternatives to CMOS technology to overcome the scaling limit, emerging technologies have demonstrated their unique features which, besides improving circuit performance, can simplify circuit structure for security purposes such as IP protection and Trojan detection. While most work with emerging technologies for security purposes to date has been with implementations like Physical Unclonable Functions (PUFs). PUFs essentially leverage device-to-device process variation. In some sense this suggests that noisier devices are more useful. Orthogonal to these efforts, we propose to leverage the unique properties of emerging technologies, other than relying on noisy devices, for IP protection and hardware attack prevention. Various sample designs have been proposed including SiNW FET based camouflaging layout and polymorphic gates for IP protection, SymFET circuit protectors against fault injection attacks, and lightweight SymFET based XOR for cryptographic systems.