Publications

This page contains selected talks, papers, and other publications.

Google Scholar Profile

2022

  • Payas Awadhutkar, Ahmed Tamrawi, RyanGoluch, Suresh Kothari. Control Flow Equivalence Method for Establishing Sanctity of Compiling. Computers & Security, January 2022.
    Paper: [Abstract] [Paper]

Compiler trap doors constitute a longstanding security problem for which there is currently no good solution. This paper presents a practical approach that shifts the focus from compiler correctness in its entirety to compiler correctness for a particular software. The guarantee is that the compiled binary's control flow is consistent with the source's control flow for a software of interest. We present an automated method to establish the equivalence by checking whether the source and the binary control flow graphs (CFGs) are isomorphic after semantics preserving graph transformations. The automated method produces evidence that can enable and simplify manual cross-checking as required to qualify an automated tool for safety-critical applications. We believe the proposed control equivalence method and its automation would be equally useful in avionics, automotive, medical devices and other safety-critical software industries where establishing trust in the binary code is critically important.

2019

  • Ahmed Tamrawi. Demystifying Software Security: A Euler’s Method Approach for Analyzing Complex Software Birzeit University, Ramallah, Palestine, October 2019.
    Paper: [Abstract] [Slides]

This talk covers the following topics: (1) the importance of software security, (2) contemporary approaches to software analysis, (3) intractability and challenges of software analysis, (4) the need for intelligence amplifying (IA) tools for practical software analysis, (5) Atlas as a novel IA tool for software analysis, and (6) research directions based on experience on multi-million DARPA programs.

2018

This 2018 DOCGEN Challenge paper describes DynaDoc, an automated documentation system for on-demand context-specific documentation. A key novelty is the use of graph database technology with an eXtensible Common Software Graph Schema (XCSG). Using XCSG-based query language, DynaDoc can mine efficiently and accurately a variety of program artifacts and graph abstractions from millions of lines of code to provide semantically relevant and rich documentation. DynaDoc leverages the extensibility of XCSG to incorporate information about commits, issues, and other supplementary artifacts and links that information to program artifacts.

Many software engineering tasks require analysis and verification of all behaviors relevant to the task. For example, all relevant behaviors must be analyzed to verify a safety or security property. An efficient algorithm must compute the relevant behaviors directly without computing all the behaviors. This is crucial in practice because it is computationally intractable if one were to compute all behaviors to find the subset of relevant behaviors.

We present a mathematical foundation to define relevant behaviors and introduce the Projected Control Graph (PCG) as an abstraction to directly compute the relevant behaviors. We developed a PCG toolbox to facilitate the use of the PCG for program comprehension, analysis, and verification. The toolbox provides: (1) an interactive visual analysis mechanism, and (2) APIs to construct and use PCGs in automated analyses. The toolbox is designed to support multiple programming languages.

Using the toolbox APIs, we conducted a verification case study of the Linux kernel to assess the practical benefits of using the PCG. The study shows that the PCG-based verification is faster and can verify 99% of 66,609 instances compared to the 66% instances verified by the formal verification tool used by the Linux Driver Verification (LDV) organization. This study has revealed bugs missed by the formal verification tool. The second case study is an interactive use of the PCG Smart View to detect side-channel vulnerabilities in Java bytecode.

  • Benjamin Holland, Payas Awadhutkar, Suresh Kothari, Ahmed Tamrawi and Jon Mathews. COMB: Computing Relevant Program Behaviors. The 40th International Conference on Software Engineering (ICSE 2018), Gothenburg, Sweden, May 2018.
    Paper: [Abstract] [Paper] [Video]

The paper presents COMB, a tool to improve accuracy and efficiency of software engineering tasks that hinge on computing all relevant program behaviors.

Computing all behaviors and selecting the relevant ones is computationally intractable. COMB uses Projected Control Graph (PCG) abstraction to derive the relevant behaviors directly and efficiently. The PCG is important as the number of behaviors relevant to a task is often significantly smaller than the totality of behaviors.

COMB provides extensive capabilities for program comprehension, analysis, and verification. We present a basic case study and a Linux verification study to demonstrate various capabilities of COMB and the addressed challenges. COMB is designed to support multiple programming languages. We demonstrate it for C and Java.

  • Suresh Kothari, Ganesh Santhanam, Benjamin Holland, Payas Awadhutkar, and Jon Mathews, Ahmed Tamrawi. Catastrophic Cyber-Physical Malware. Springer Verlag Publishers, April 2018.
    Book Chapter: [Abstract] [Chapter]

With the advent of highly sophisticated cyber-physical malware (CPM) such as Industroyer, a cyberattack could be as destructive as the terrorist attack on 9/11, it would virtually paralyze the nation. We discuss as the major risks the vulnerability of: telecommunication infrastructure, industrial control systems (ICS), and mission-critical software.

In differentiating CPM from traditional malware, the difference really comes from the open-ended possibilities for malware triggers resulting from the wide spectrum of sensor inputs, and the almost limitless application-specific possibilities for designing malicious payloads.

Fundamentally, the challenges of detecting sophisticated CPM stem from the complexities inherent in the software at the heart of cyber-physical systems. We discuss three fundamental challenges: explosion of execution behaviors, computational intractability of checking feasible behaviors, and difficult-to-analyze programing constructs.

In detecting novel CPM, the tasks are: developing plausible hypotheses for malware trigger and mali- cious payload, analyzing software to gather evidence based on CPM hypotheses, and verifying software to prove or refute a hypothesis based on the gathered evidence. We discuss research directions for effective automation to support these tasks.

2017

Verifying software in mission-critical Cyber-Physical Systems (CPS) is an important but daunting task with challenges of accuracy and scalability. This paper discusses lessons learned from verifying properties of the Linux kernel. These lessons have raised questions about traditional verification approaches, and have led us to a model-based approach for software verification. These models are high-level models of the software, as opposed to the prevalent formal methods with low-level representations of software. We use models to gain insights into software verification challenges and use those insights to improve software verification. We demonstrate significant advantages of models with a Linux kernel study involving verification of 66,609 Lock instances. We use models to: (a) analyze and find flaws in verification results from LDV, a top-rated Linux verification tool, (b) show significant improvement over LDV by improving accuracy, speed, and by verifying 99.3% instances compared to 65.7% instances by LDV.

2016

  • Ahmed Tamrawi, Suresh Kothari. Projected Control Graph for Accurate and Efficient Analysis of Safety and Security Vulnerabilities. The 23rd Asia-Pacific Software Engineering Conference (APSEC 2016), Hamilton, New Zealand, December 2016.
    Paper: [Abstract] [Paper]

The goal of path-sensitive analysis (PSA) is to achieve accuracy by accounting precisely for the execution behavior along each path of a control flow graph (CFG). A practical adoption of PSA is hampered by two roadblocks: (a) the exponential growth of the number of CFG paths, and (b) the exponential complexity of a path feasibility check. We introduce projected control graph (PCG) as an optimal mathematical abstraction to address these roadblocks.

The PCG follows from the simple observation that for any given analysis problem, the number of distinct relevant execution behaviors may be much smaller than the number of CFG paths. The PCG is a projection of the CFG to retain only the relevant execution behaviors and elide duplicate paths with identical execution behavior. A mathematical definition of PCG and an efficient algorithm to transform CFG to PCG are presented.

We present an empirical study for three major versions of the Linux kernel to assess the practical benefit of using the optimal mathematical abstraction. As a measure of the efficiency gain, the study reports the reduction from CFG to PCG graphs for all relevant functions for pairing Lock and Unlock on all feasible execution paths. We built a tool to compute these graphs for 66,609 Lock instances. The CFG and PCG graphs with their source correspondence are posted on a website. We used these PCG graphs in a classroom project to audit the results of Lock and Unlock pairing done by the Linux Driver Verification (LDV) tool, the top-rated formal verification tool for the Linux kernel. Our audit has revealed complex Linux bugs missed by LDV.

  • Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi. Insights for Practicing Engineers from a Formal Verification Study of the Linux Kernel. The 2016 IEEE International Symposium on Software Reliability Engineering Workshops ISSREW 2016, Ottawa, Canada, October 2016.
    Paper: [Abstract] [Paper]

Formal verification of large software has been an illusive target, riddled with the problem of scalability. Even if the obstacle of scale may be cleared, major challenges remain to adopt formal verification in practice. This paper presents an empirical study using a top-rated formal verification tool for Linux, and draws insights from the study to discuss the intrinsic challenges for adopting formal verification in practice. We discuss challenges that focus on practical needs: (a) facilitate crosschecking of verification results, (b) enable the use of formal verification for certification, and (c) integrate formal methods in a development environment. Leaning on visionary papers by Turing Award recipients, we present novel ideas for advancing formal verification in new directions that would help practicing engineers.

Formal verification of large software has been an elusive target, riddled with problems of low accuracy and high computational complexity. With growing dependence on software in embedded and cyber-physical systems where vulnerabilities and malware can lead to disasters, an efficient and accurate verification has become a crucial need. The verification should be rigorous, computationally efficient, and automated enough to keep the human effort within reasonable limits, but it does not have to be completely automated. The automation should actually enable and simplify human cross-checking which is especially important when the stakes are high. Unfortunately, formal verification methods work mostly as automated black boxes with very little support for cross-checking.

This thesis is about a different way to approach the software verification problem. It is about creating a powerful fusion of automation and human intelligence by incorporating algorithmic innovations to address the major challenges to advance the state of the art for accurate and scalable software verification where complete automation has remained intractable. The key is a mathematically rigorous notion of verification-critical evidence that the machine abstracts from software to empower human to reason with. The algorithmic innovation is to discover the patterns the developers have applied to manage complexity and leverage them. A pattern-based verification is crucial because the problem is intractable otherwise. We call the overall approach Evidence-Enabled Verification (EEV).

This thesis presents the EEV with two challenging applications: (1) EEV for Lock/Unlock Pairing to verify the correct pairing of mutex lock and spin lock with their corresponding unlocks on all feasible execution paths, and (2) EEV for Allocation/Deallocation Pairing to verify the correct pairing of memory allocation with its corresponding deallocations on all feasible execution paths. We applied the EEV approach to verify recent versions of the Linux kernel. The results include a comparison with the state-of-the-art Linux Driver Verification (LDV) tool, effectiveness of the proposed visual models as verification-critical evidence, representative examples of verification, the discovered bugs, and limitations of the proposed approach.

  • Suresh Kothari, Ahmed Tamrawi, Jon Mathews. Human-machine resolution of Invisible Control Flow?. The IEEE 24th International Conference on ICPC 2016, Austin, Texas, May 2016.
    Paper: [Abstract] [Paper]

Invisible Control Flow (ICF) results from dynamic binding and asynchronous processing. For modern software replete with ICF, the ability to analyze and resolve ICF is crucial for verifying software. A fully automated analysis to resolve ICF suffers from imprecision and high computational complexity. As a practical alternative, we present a novel solution of interactive human-machine collaboration to resolve ICF. Our approach is comprised of interactive program analysis and comprehension to systematically capture and link the clues crucial for resolving ICF. We present the tool support we have developed using the query language and visualization capabilities of the Atlas Platform. We illustrate the approach using examples where resolving ICF is crucial to verify software and show a complex bug in the Linux kernel discovered by resolving ICF.

  • Suraj Kothari, Ahmed Tamrawi, Jeremias Sauceda, Jon Mathews. Let’s Verify Linux: Accelerated Learning of Analytical Reasoning through Automation and Collaboration. The 2016 IEEE/ACM International Conference on Software Engineering Companion ICSE-C, Austin, Texas, May 2016.
    Paper: [Abstract] [Paper]

We describe our experiences in the classroom using the internet to collaboratively verify a significant safety and security property across the entire Linux kernel. With 66,609 instances to check across three versions of Linux, the naive approach of simply dividing up the code and assigning it to students does not scale, and does little to educate. However, by teaching and applying analytical reasoning, the instances can be categorized effectively, the problems of scale can be managed, and students can collaborate and compete with one another to achieve an unprecedented level of verification. We refer to our approach as Evidence-Enabled Collaborative Verification (EECV). A key aspect of this approach is the use of visual software models, which provide mathematically rigorous and critical evidence for verification. The visual models make analytical reasoning interactive, interesting and applicable to large software. Visual models are generated automatically using a tool we have developed called L-SAP. This tool generates an Instance Verification Kit (IVK) for each instance, which contains all of the verification evidence for the instance. The L-SAP tool is implemented on a software graph database platform called Atlas. This platform comes with a powerful query language and interactive visualization to build and apply visual models for software verification. The course project is based on three recent versions of the Linux operating system with altogether 37 MLOC and 66,609 verification instances. The instances are accessible through a website for students to collaborate and compete. The Atlas platform, the L-SAP tool, the structured labs for the project, and the lecture slides are available upon request for academic use.

  • Suraj Kothari, Ahmed Tamrawi, Jon Mathews. Rethinking Verification: Accuracy, Efficiency, and Scalability through Human-Machine Collaboration. The 2016 IEEE/ACM International Conference on Software Engineering Companion ICSE-C, Austin, Texas, May 2016.
    Paper: [Abstract] [Paper]

With growing dependence on software in embedded and cyber-physical systems where vulnerabilities and malware can lead to disasters, efficient and accurate verification has become a crucial need for safety and cybersecurity. Formal verification of large software has remained an elusive target, riddled with problems of low accuracy and high computational complexity. The need for automating verification is undoubted, however human is indispensable to accurate real-world software verification. The automation should actually enable and simplify human cross-checking, which is especially important when the stakes are high. This technical briefing discusses the challenges of creating a powerful fusion of automation and human intelligence to solve software verification problems where complete automation has remained intractable. We will contrast with existing software verification approaches and reflect on their strengths and limitations as a human-machine collaboration framework and outline key software engineering research and practice challenges to be addressed in the future.

2014

  • Suresh Kothari, Akshay Deepak, Ahmed Tamrawi, Benjamin Holland, Sandeep Krishnan. A “Human-in-the-loop” Approach for Resolving Complex Software Anomalies. The 2014 IEEE International Conference on Systems, Man, and Cybernetics (SMC 2014), San Diego, California, October 2014.
    Paper: [Abstract] [Paper]

Automated static analysis tools are widely used in identifying software anomalies, such as memory leak, unsafe thread synchronization and malicious behaviors in smartphone applications. Such anomaly-prone scenarios can be bifurcated into: "ordinary" (analysis requires relatively simple automation) and "complex" (analysis poses extraordinary automation challenges). While automated static analysis tools can resolve ordinary scenarios with high accuracy, automating the analysis of complex scenarios can be very challenging and, at times, infeasible. Even when feasible the cost for full automation can be exorbitant: either in implementing the automation or in sifting through the large number of erroneous results manually. Instead, we appeal for a "Human-in-the-loop" approach called "Amplified Reasoning Technique" (ART). While some of the existing approaches do involve human in the analysis process, the roles played by man and machine are mainly segregated. Whereas, ART puts man and machine in a "loop" in an interactive and visualization-based fashion. This paper makes an attempt to convince its readers to make their analysis of software anomalies ART-based by presenting real-world case studies of complex anomalies and how an ART based approach can be very effective in resolving them. The case studies highlight the desired characteristics of an ART based tool and the type of role it plays in amplifying human intelligence.

2012

  • Ahmed Tamrawi, Hoan Anh Nguyen, Hung Viet Nguyen, Tien N Nguyen. SYMake: A Build Code Analysis and Refactoring Tool for Makefiles. The 27th IEEE/ACM International Conference on Automated Software Engineering ASE 2012, Essen, Germany, September 2012.
    Paper: [Abstract] [Paper]

Software building is an important task during software development. However, program analysis support for build code is still limited, especially for build code written in a dynamic language such as Make. We introduce SYMake, a novel program analysis and refactoring tool for build code in Makefiles. SYMake is capable of detecting several types of code smells and errors such as cyclic dependencies, rule inclusion, duplicate prerequisites, recursive variable loops, etc. It also supports automatic build code refactoring, e.g. rule extraction/removal, target creation, target/variable renaming, prerequisite extraction, etc. In addition, SYMake provides the analysis on defined rules, targets, prerequisites, and associated information to help developers better understand build code in a Makefile and its included files.

  • Ahmed Tamrawi, Hoan Anh Nguyen, Hung Viet Nguyen, Tien N Nguyen. Build Code Analysis with Symbolic Evaluation. The 34th International Conference on Software Engineering ICSE 2012, Zurich, Switzerland, June 2012.
    Paper: [Abstract] [Paper]

Build process is crucial in software development. However, the analysis support for build code is still limited. In this paper, we present SYMake, an infrastructure and tool for the analysis of build code in make. Due to the dynamic nature of make language, it is challenging to understand and maintain complex Makefiles. SYMake provides a symbolic evaluation algorithm that processes Makefiles and produces a symbolic dependency graph (SDG), which represents the build dependencies (i.e. rules) among files via commands. During the symbolic evaluation, for each resulting string value in an SDG that represents a part of a file name or a command in a rule, SYMake provides also an acyclic graph (called T-model) to represent its symbolic evaluation trace. We have used SYMake to develop algorithms and a tool 1) to detect several types of code smells and errors in Makefiles, and 2) to support build code refactoring, e.g. renaming a variable/target even if its name is fragmented and built from multiple substrings. Our empirical evaluation for SYMake's renaming on several real-world systems showed its high accuracy in entity renaming. Our controlled experiment showed that with SYMake, developers were able to understand Makefiles better and to detect more code smells as well as to perform refactoring more accurately.

  • Anh Tuan Nguyen, Tung Thanh Nguyen, Hoan Anh Nguyen, Ahmed Tamrawi, Hung Viet Nguyen, Jafar Al-Kofahi, Tien N Nguyen. Graph-Based Pattern-Oriented, Context-Sensitive Source Code Completion. The 34th International Conference on Software Engineering ICSE 2012, Zurich, Switzerland, June 2012.
    Paper: [Abstract] [Paper]

Code completion helps improve developers' programming productivity. However, the current support for code completion is limited to context-free code templates or a single method call of the variable on focus. Using software libraries for development, developers often repeat API usages for certain tasks. Thus, a code completion tool could make use of API usage patterns. In this paper, we introduce GraPacc, a graph-based, pattern-oriented, context-sensitive code completion approach that is based on a database of such patterns. GraPacc represents and manages the API usage patterns of multiple variables, methods, and control structures via graph-based models. It extracts the context-sensitive features from the code under editing, e.g. the API elements on focus and their relations to other code elements. Those features are used to search and rank the patterns that are most fitted with the current code. When a pattern is selected, the current code will be completed via a novel graph-based code completion algorithm. Empirical evaluation on several real-world systems shows that GraPacc has a high level of accuracy in code completion.

2011

Software bugs are inevitable and bug fixing is an essential and costly phase during software development. Such defects are often reported in bug reports which are stored in an issue tracking system, or bug repository. Such reports need to be assigned to the most appropriate developers who will eventually fix the issue/bug reported. This process is often called Bug Triaging.

Manual bug triaging is a difficult, expensive, and lengthy process, since it needs the bug triager to manually read, analyze, and assign bug fixers for each newly reported bug. Triagers can become overwhelmed by the number of reports added to the repository. Time and efforts spent into triaging typically diverts valuable resources away from the improvement of the product to the managing of the development process.

To assist triagers and improve the bug triaging efficiency and reduce its cost, this thesis proposes Bugzie, a novel approach for automatic bug triaging based on fuzzy set and cachebased modeling of the bug-fixing capability of developers. Our evaluation results on seven large-scale subject systems show that Bugzie achieves significantly higher levels of efficiency and correctness than existing state-of-the-art approaches. In these subject projects, Bugzie's accuracy for top-1 and top-5 recommendations is higher than those of the second best approach from 4-15% and 6-31%, respectively as Bugzie's top-1 and top-5 recommendation accuracy is generally in the range of 31-51% and 70-83%, respectively. Importantly, existing approaches take from hours to days (even almost a month) to finish training as well as predicting, while in Bugzie, training time is from tens of minutes to an hour.

  • Ahmed Tamrawi, Tung Thanh Nguyen, Jafar Al-Kofahi, Tien N Nguyen. Fuzzy Set and Cache-Based Approach for Bug Triaging. The 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering ESEC/FSE 2011, Szeged, Hungary, September 2011.
    Paper: [Abstract] [Paper]

Bug triaging aims to assign a bug to the most appropriate fixer. That task is crucial in reducing time and efforts in a bug fixing process. In this paper, we propose Bugzie, a novel approach for automatic bug triaging based on fuzzy set and cache-based modeling of the bug-fixing expertise of developers. Bugzie considers a software system to have multiple technical aspects, each of which is associated with technical terms. For each technical term, it uses a fuzzy set to represent the developers who are capable/competent of fixing the bugs relevant to the corresponding aspect. The fixing correlation of a developer toward a technical term is represented by his/her membership score toward the corresponding fuzzy set. The score is calculated based on the bug reports that (s)he has fixed, and is updated as the newly fixed bug reports are available. For a new bug report, Bugzie combines the fuzzy sets corresponding to its terms and ranks the developers based on their membership scores toward that combined fuzzy set to find the most capable fixers. Our empirical results show that Bugzie achieves significantly higher accuracy and time efficiency than existing state-of-the-art approaches.

2010

  • Ahmed Tamrawi, Tung Thanh Nguyen, Jafar Al-Kofahi, Tien N Nguyen. Fuzzy Set-Based Automatic Bug Triaging (NIER Track). The 33rd International Conference on Software Engineering ICSE 2010, Cape Town, South Africa, May 2010.
    Paper: [Abstract] [Paper]

Assigning a bug to the right developer is a key in reducing the cost, time, and efforts for developers in a bug fixing process. This assignment process is often referred to as bug triaging. In this paper, we propose Bugzie, a novel approach for automatic bug triaging based on fuzzy set-based modeling of bug-fixing expertise of developers. Bugzie considers a system to have multiple technical aspects, each is associated with technical terms. Then, it uses a fuzzy set to represent the developers who are capable/competent of fixing the bugs relevant to each term. The membership function of a developer in a fuzzy set is calculated via the terms extracted from the bug reports that (s)he has fixed, and the function is updated as new fixed reports are available. For a new bug report, its terms are extracted and corresponding fuzzy sets are union'ed. Potential fixers will be recommended based on their membership scores in the union'ed fuzzy set. Our preliminary results show that Bugzie achieves higher accuracy and efficiency than other state-of-the-art approaches.

  • Jafar M Al-Kofahi, Ahmed Tamrawi, Tung Thanh Nguyen, Hoan Anh Nguyen, Tien N Nguyen. Fuzzy Set Approach for Automatic Tagging in Evolving Software. The 2010 IEEE International Conference on Software Maintenance ICSM 2010, Timișoara, Romania, September 2010.
    Paper: [Abstract] [Paper]

Software tagging has been shown to be an efficient, lightweight social computing mechanism to improve different social and technical aspects of software development. Despite the importance of tags, there exists limited support for automatic tagging for software artifacts, especially during the evolutionary process of software development. We conducted an empirical study on IBM Jazz's repository and found that there are several missing tags in artifacts and more precise tags are desirable. This paper introduces a novel, accurate, automatic tagging recommendation tool that is able to take into account users' feedbacks on tags, and is very efficient in coping with software evolution. The core technique is an automatic tagging algorithm that is based on fuzzy set theory. Our empirical evaluation on the real-world IBM Jazz project shows the usefulness and accuracy of our approach and tool.