Convolutional neural network designed as small truth tables, application to cryptography, formal verification & explainability

• Main Author: Benamira, Adrien
• Other Authors: Thomas Peyrin
• Format: Thesis-Doctor of Philosophy
• Language: English
• Published: Nanyang Technological University 2024
• Subjects: Computer and Information Science; Mathematical Sciences; Deep convolutional neural network; Machine/deep learning; Cryptanalysis; Neural distinguisher; Exact global xplainability; Side-channel attacks; Fully homomorphic encryption
• Online Access: https://hdl.handle.net/10356/177203
• Institution: Nanyang Technological University

DCNNs have revolutionized machine learning (ML) and deep learning (DL), achieving remarkable success in image recognition, natural language processing, and other domains. However, their deployment in security-critical industries such as cybersecurity, energy, finance, and the military faces persistent safety and reliability issues. This thesis addresses three primary challenges: the absence of global and precise interpretability in DCNNs, the need for exact, comprehensive, sound, and efficient formal verification of DCNN properties, and the looming privacy threat to user input in cloud-based DCNN deployments for sensitive data. Our research aims to enhance the transparency, reliability, and security of DCNNs, facilitating their wider adoption in critical real-world applications. This thesis first investigates the potential synergy between cryptanalysis and AI, leveraging deep neural networks (DNNs) to create an automatic cryptographic distinguisher. However, the resulting neural distinguisher (ND) inherits the opacity of DNNs, prompting us to address the “black-box” challenge. Our effort to tackle this very important explainability problem on a mathematically well-defined and small binary size input problem led to the design of methods never before invented in the field of ML/DL. Our approach is inspired by the principles of cipher design. In SPN cipher design, a small cryptographic component known as an S-box (whose input/output sizes usually range from 4 bits to 8 bits) plays a pivotal role in achieving efficient implementation and amenable security analysis, enabling the approximation of large random permutation functions with security guarantees. Building upon this concept, our thesis explores the application of similar principles to the DL field. Our specific aim is to design and develop a compact and small learnable filter for convolutional neural networks (CNNs), with bit widths ranging from 9-bit to 1-bit or 16-bit to 1-bit. When these small filters are assembled into layers and layers into DCNNs, our goal is to enable the efficient approximation of large non-random functions, such as image classifiers. Overall, we managed to reduce the size of elementary building blocks within CNN architectures, making them as analyzable as encryption blocks (S-boxes) for both analytical and implementation purposes. This study is designed to harmonize cryptanalysis and ML/DL by reconceptualizing bulky CNN filter functions in DL into the streamlined, S-box-like structures favored in cryptanalysis. The innovation lies in creating a dual-purpose neural network operator: one that ML/DL engineers can efficiently train on diverse datasets and subsequently, after training, convert into a format security experts can intuitively scrutinize and fortify. Our approach introduces a novel convolution filter neural network operator, known as the Learnable Truth Table (LTT) filter. First and foremost, our LTT filter is designed to be (i) fully exhaustible in practical time, (ii) learnable, and (iii) easily integrable into an LTT layer and LTT layers easily integrable into a network which we call TTNet. Second, TTNet needs to be scalable on large-scale input instances and complex tasks, enhancing its usefulness in real-world applications. These rules enable the LTT filter to be differentiable while also allowing for the computation of its complete distribution in just \(2^{16}\) operations before deployment. The versatility of this LTT filter lies in its ability to be converted, after training, into various forms, including a truth table, conjunctive normal form (CNF), disjunctive normal form (DNF), algebraic normal form (ANF), optimal implementation in Boolean gates (optimal if the computation of its complete distribution can be done in less than \(2^{12}\) operations), Boolean rule, and reduced ordered binary decision diagram (ROBDD). This flexibility allows the entire TTNet DCNN to be transformed into an interconnected truth table network, CNFs/DNFs/ANFs, an optimal Boolean gate circuit, a rule-based model, or a sum of ROBDDs. In the second part of the thesis, we show that the family of Truth Table nets offers an efficient solution to the challenge of analyzing DCNNs. The LTT filter bridges traditional symbolic AI and new learning AI trends. Indeed, symbolic AI is known for being rule-based, explainable, compact, and proven, with the truth table being a standard tool. On the other hand, learning AI is known for being automatable and scalable on complex tasks, with the learnable CNN filter being a standard tool. The LTT filter is a differentiable logic tool that combines the strengths of both AI approaches. This research extends the application of TTNet to various domains, demonstrating its scalability and effectiveness, notably in classifying large-scale image datasets such as ImageNet. Furthermore, TTNet stands out for its compactness among state-of-the-art differentiable logic gate DNNs, offering an efficient solution for Boolean logic gate circuits conversion of DNNs. Moving beyond foundational capabilities, we have developed four distinct variations of TTNet (TTVerif, TTRules, TT-SCA, TT-FHE) to address specific challenges across four applications. TTVerif shows our network's ability to perform formal, exact, complete, and sound verification of adversarial attack robustness properties across various noise levels. TTRules applies TTNet's principles to complex tabular data from financial, genetic, and healthcare sectors, aiming for global exact interpretability. In the realm of side-channel attacks (SCA), TT-SCA elucidates DNN behavior, identifying critical points of masking and leakage. Lastly, TT-FHE evidences TTNet's potential to secure user data privacy in cloud deployments through fully homomorphic encryption (FHE). These adaptations underscore TTNet's broad applicability and its capacity to solve multifaceted problems in and beyond cryptography. To conclude, this thesis demonstrates the applicability of TTNet to image classification tasks, mono-channel time series classification tasks, tabular datasets classification and regression tasks, and various critical security applications. TTNet uniquely combines compactness, verification, interpretability, and privacy preservation. The thesis aimed to develop a versatile and robust neural network operator (LTT filter) that bridges symbolic AI and learning AI, facilitating deployments in environments where safety is paramount, thereby rendering it a valuable tool for regulation.