Application & Network Security
Session Title | Demystifying Software Security: A Euler's Method Approach for Analyzing Complex Software
"Nowadays the imminent danger of cyber-physical malware (CPM) is evident from attacks such as the power outage in Ukraine, or the hijacking of a Jeep Cherokee. The traditional notion of malware is too narrow, and the prevalent characterizations (virus, worm, Trojan horse, spyware etc.) are neither precise nor comprehensive enough to characterize cyber-physical malware. Detecting sophisticated CPM is like searching for a needle in the haystack without knowing what the needle looks like. The talk will be about congregate interdisciplinary knowledge to describe the fundamentals of CPM, the mathematical foundation for analyzing and verifying CPM, the state-of-the-art software analysis approaches and inherent challenges, and directions for future research. Employing real-world examples, we shall illustrate the challenges of analyzing and verifying CPM.
The security problems are often rooted in the complex software. Therefore, it is important to demystify software security, so that software engineers and security practitioners can understand the inherent challenges of contemporary approaches to advance the software analysis and verification techniques to effectively address the CPM problems.
The talk will be shaped from the perspective of crucial needs for modeling, analyzing, and verifying CPM. It will cover:
- Modeling: The Confidentiality-Integrity-Availability (CIA) triad characterizes the impact of the malware but it is not meant to facilitate analysis or verification of software. Modeling research is needed to characterize the program artifacts that enact CPM.
- Analysis: Complete automation and machine learning are emphasized in many current research approaches to analyze software for security. The talk will illustrate the shortcomings of such techniques and reflect on the need for a new type of analysis to address CPM.
- Verification: Given the complexity of CPM and the possibility of catastrophic consequences, we will discuss the need for transparent verification that enable a human to easily participate by cross checking the tool results or completing the verification where automation falls short."
Ahmed Tamrawi is a software security researcher, instructor, and a full-stack developer. He has extensive experience in program analysis to: (1) verify the safety and security of industrial software such as the Linux kernel, and (2) detect novel and sophisticated algorithmic complexity and side channel attacks in Java applications and malware in Android applications. Ahmed also has experience working on two high profile US Department of Defense DARPA programs: Automated Program Analysis for Cybersecurity (APAC) and Space/Time Analysis for Cybersecurity (STAC) programs.
Ahmed Tamrawi is currently a research scientist at EnSoft Corp. and an assistant professor at Birzeit University. At EnSoft Corp., Ahmed is working on advancing Atlas and Modelify. Atlas is a novel program analysis platform and Modelify is a novel conversion tool from C code to Simulink models. His past work experience includes: assistant professor at Yarmouk University, a software development engineer intern at Amazon, a research and teaching assistant at Iowa State University, research and development engineer at G.ho.st, and software development engineer intern at MBRM
Ahmed holds a PhD and MSc degrees in Computer Engineering from Iowa State University, and B.S in Computer Engineering from Yarmouk University. His MSc research was focused on developing novel bug triaging and build code analyses. His PhD research resulted on the development of a novel compact software graph called the Projected Control Graph and the design of the L-SAP tool for fast, scalable, and efficient evidence-enabled verification for the Linux kernel.
Want to find more about Ahmed, then read through his Teaching Statement, Reasearch Statement, and Two-Page CV.