QCE'26
Ali Hamza Malik
Provable Security for Emerging Systems
PhD Candidate in Electrical & Computer Engineering at University of Massachusetts Amherst.
My expertise are in formal methods and security verification where I use math and formal models to prove critical systems won't fail in the worst possible ways.
About Me
Hi, I am a PhD Candidate in Electrical & Computer Engineering @ University of Massachusetts Amherst. I work on formal methods, security verification, and model checking with Dr. Muhammad Taqi Raza in Khwarizmi Lab.
I study the formal specifications of large-scale network and communication systems for identifying vulnerabilities and mitigating risks like unauthorized access and denial-of-service. My research focuses on conducting comprehensive and systematic security analyses of modern digital systems through SAT-based bounded model checking and theorem proving. This includes scrutinizing the security functions and protocols within the U.S. ACH network, quantum-classical interfaces (QKD), and cross-plane eSIM connectivity to ensure the highest standard of protection for users and business assets. A systematic analysis of these security specifications not only enhances the resilience of systems but also ensures mathematically proven validation for complex control planes.
My research paves the way for the development of effective remedies, ensuring the integrity and trustworthiness of digital systems in various operational contexts.
Before joining UMass, I completed my Bachelor’s in Electrical Engineering (BE) from National University of Sciences and Technology (NUST) in 2023. At NUST, I worked as an Undergraduate Research Assistant and Hardware Security Intern, focusing on autonomous aerial swarm robotics and logic-locking defenses for hardware security. Further details regarding my technical deployments and publications are in my CV.
Research Interests
Formal methods and security analysis
Systematic analysis of large-scale deployed systems, modeling protocol stacks against their specifications to uncover access-control and trust-boundary gaps the specification never states
Reliability of large language models
Making behavioral properties verifiable, from whether a thinking trace reflects the computation behind an answer to whether single-call guarantees survive multi-step agentic trajectories
Quantum and post-quantum security
Where quantum and post-quantum deployments break at the classical boundary, in control planes, key management, and migration paths, rather than in the cryptographic primitive itself
Experience
Graduate Research Assistant
September 2023 - Present
Khwarizmi Lab, University of Massachusetts Amherst • Amherst, MA
- Built a verification framework to analyze quantum key distribution (QKD) protocols; identified three new vulnerabilities arising from quantum-classical interactions
- Applied formal analysis to U.S. ACH banking systems to uncover security vulnerabilities in the access control and authorization of ACH direct payments
Undergraduate Research Assistant
September 2022 - July 2023
Communication Systems and Networks Lab, NUST
- Collaborated in the design and implementation of an event-driven coordination protocol for multi-agent aerial swarms on Raspberry Pi companion computers with Pixhawk/ArduPilot flight controllers
- Designed and optimized leader-follower formation control (flock, line, helical) with dynamic reconfiguration, achieving under 2 min formation-switching latency
- Engineered a mesh networking stack (IEEE 802.11, UDP/TCP, MAVLink) to enable fault-tolerant communication for control coordination in real-time (under 100 ms latency)
Hardware Security Intern
June 2022 - September 2022
IC Design Lab, NUST
- Led the design of ENIGMA, a Python framework that automatically inserts logic-locking defenses into hardware designs, protecting IP designs from unauthorized use and reverse engineering
- Designed a parametrized key-insertion system (64-256 bits) with user-defined cell libraries to analyze the impact of logic obfuscation on a chip's area, delay, and power
Machine Learning Intern
June 2021 - September 2021
TUKL Deep Learning Lab, NUST
- Implemented an automated pipeline to extract, structure, and preprocess raw court documents
- Fine-tuned Transformer-based models for court-case outcome prediction achieving 83% accuracy
Selected Publications
publications in reversed chronological order.