Adaptive & Secure Computing Systems (ASCS) Laboratory

FHEON: A Configurable Framework for Developing Privacy-Preserving Neural Networks Using Homomorphic Encryption

Privacy-preserving machine learning seeks to protect the confidentiality of both data and models, ensuring that sensitive information remains secure throughout training and inference. Although Homomorphic Encryption is regarded as one of the most promising approaches for this purpose, there is still a lack of configurable frameworks that enable the development of privacy-preserving applications comparable to those available in conventional machine learning.

Researchers at the Lab are developing FHEON, an open-source framework designed to enable privacy-preserving neural network training and inference using Homomorphic Encryption. The research focuses on designing and implementing new and more efficient FHE-friendly algorithms for fundamental machine learning primitives. FHEON provides a suite of encrypted computation efficient primitives, including support for Encrypted Convolutional Neural Networks, Spiking Neural Networks, High-Throughput Batched Neural Networks, and privacy-preserving Training mechanisms.

Sub projects: FHEON, PrivSpike, SentinalTouch, VIPER

HERISCV: Homomorphic-Encryption Enabled RISC-V Architecture

Large Arithmetic Word Size (LAWS): Word size directly relates to the signal-to-noise ratio (SNR) of how a ciphertext is stored and manipulated in computation. There currently is no hardware architecture that natively supports the register sizes and/or the execution units performing the fundamental mathematical and logical operations for lattice FHE schemes
ISA Based Reconfigurable Architecture: Given the evolving state of improvements and new schemes in the field of FHE, the HERISCV architecture aims to provide an array of operations and functionality instead of optimizing the hardware for one particular algorithm. The architecture provides significant performance gains for lattice-based FHE applications as well as the flexibility to experiment with new designs by having instruction support for the core operations, e.g., lattices, polynomials, arithmetic, logic and finite fields.

Post-Quantum Cryptographic Acceleration, Formal Verification, and Applications

At the Lab, we are focused on advancing the security and efficiency of Post-Quantum Cryptography (PQC) through the support of accelerated PQC, formal verification, and practical application development. We design and provide hardware modules for leading PQC families, including lattice-based, isogeny-based, and hash-based cryptography. Our work adhere closely to the NIST standardization guidelines, ensuring that PQC solutions are applicable, usable, and deployable across a wide range of applications and hardware platforms.

Our research team is also dedicated to the secure implementation of PQC algorithms. This work includes the formalization of NIST standardized schemes to guarantee both functional correctness and side-channel resistance. Beyond implementation, we actively explore algorithmic innovations and extensions of PQC primitives for emerging domains. A key example is our efforts to integrate PQC into low-power, connected IoT and distributed systems, where performance and security must coexist under strict resource constraints.

FAKAZI: Formal Infrastructure for the Development and Verification of Secure and Trust Critical Systems

Formal verification serves as a fundamental pillar for ensuring the reliability and security of computing systems. This work presents Fakazi, a novel infrastructure designed to address the challenges hindering the widespread adoption of formal verification. Fakazi offers a versatile FV engine and user-friendly environment tailored for verifying critical systems with main focus on security vulnerabilities.

Fakazi contain two main components: Static Analyzer and Dynamic Analyzer. The static analyzer leverages automated theorem provers to reason about program correctness at the source level, while the dynamic analyzer employs dynamic binary analysis. It employs a Fuzzying guided engine depending on Symbolic Execution and SMT solvers to verify runtime behavior and uncover potential security vulnerabilities such as memory and constant-time violations.

This infrastructure is also developed to abstract the complexity of formal verification from the development of critical system. Our goal is to ensure provable correctness, trust, security, and robustness from algorithm design to implementation. This infrastructure should automatically supports formally verified primitives for PQC, FHE, and ZKP systems, while enhancing automation and scalability within the verification pipeline.

Sub Projects: Fakazi, FAVE, DALC-CT