Zheng Leong Chua

Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel et al.

Despite the functional success of deep neural networks (DNNs), their trustworthiness remains a crucial open challenge. To address this challenge, both testing and verification techniques have been proposed. But these existing techniques provide either scalability to large networks or formal guarantees, not both. In this paper, we propose a scalable quantitative verification framework for deep neural networks, i.e., a test-driven approach that comes with formal guarantees that a desired probabilistic property is satisfied. Our technique performs enough tests until soundness of a formal probabilistic property can be proven. It can be used to certify properties of both deterministic and randomized DNNs. We implement our approach in a tool called PROVERO and apply it in the context of certifying adversarial robustness of DNNs. In this context, we first show a new attack-agnostic measure of robustness which offers an alternative to purely attack-based methodology of evaluating robustness being reported today. Second, PROVERO provides certificates of robustness for large DNNs, where existing state-of-the-art verification tools fail to produce conclusive results. Our work paves the way forward for verifying properties of distributions captured by real-world deep neural networks, with provable guarantees, even where testers only have black-box access to the neural network.

Xiaoxuan Lou, Fan Zhang, Zheng Leong Chua et al.

Rowhammer is a hardware-based bug that allows the attacker to modify the data in the memory without accessing it, just repeatedly and frequently accessing (or hammering) physically adjacent memory rows. So that it can break the memory isolation between processes, which is seen as the cornerstone of modern system security, exposing the sensitive data to unauthorized and imperceptible corruption. A number of previous works have leveraged the rowhammer bug to achieve various critical attacks. In this work, we propose a unified reference framework for analyzing the rowhammer attacks, indicating three necessary factors in a practical rowhammer attack: the attack origin, the intended implication and the methodology. Each factor includes multiple primitives, the attacker can select primitives from three factors to constitute an effective attack. In particular, the methodology further summarizes all existing attack techniques, that are used to achieve its three primitives: Location Preparation (LP), Rapid Hammering (RH), and Exploit Verification (EV). Based on the reference framework, we analyze all previous rowhammer attacks and corresponding countermeasures. Our analysis shows that how primitives in different factors are combined and used in previous attacks, and thus points out new possibility of rowhammer attacks, enabling proactive prevention before it causes harm. Under the framework, we propose a novel expressive rowhammer attack that is capable of accumulating injected memory changes and achieving rich attack semantics. We conclude by outlining future research directions.

Shweta Shinde, Zheng Leong Chua, Viswesh Narayanan et al.

New hardware primitives such as Intel SGX secure a user-level process in presence of an untrusted or compromised OS. Such "enclaved execution" systems are vulnerable to several side-channels, one of which is the page fault channel. In this paper, we show that the page fault side-channel has sufficient channel capacity to extract bits of encryption keys from commodity implementations of cryptographic routines in OpenSSL and Libgcrypt --- leaking 27% on average and up to 100% of the secret bits in many case-studies. To mitigate this, we propose a software-only defense that masks page fault patterns by determinising the program's memory access behavior. We show that such a technique can be built into a compiler, and implement it for a subset of C which is sufficient to handle the cryptographic routines we study. This defense when implemented generically can have significant overhead of up to 4000X, but with help of developer-assisted compiler optimizations, the overhead reduces to at most 29.22% in our case studies. Finally, we discuss scope for hardware-assisted defenses, and show one solution that can reduce overheads to 6.77% with support from hardware changes.