Mehdi Mirakhorli

Scientific software development demands robust solutions to meet the complexities of modern scientific systems. In response, we propose a paradigm-shifting Neuro-Symbolic Approach to Certified Scientific Software Synthesis. This innovative framework integrates large language models (LLMs) with formal methods, facilitating automated synthesis of complex scientific software while ensuring verifiability and correctness. Through a combination of technologies including a Scientific and Satisfiability-Aided Large Language Model (SaSLLM), a Scientific Domain Specific Language (DSL), and Generalized Planning for Abstract Reasoning, our approach transforms scientific concepts into certified software solutions. By leveraging advanced reasoning techniques, our framework streamlines the development process, allowing scientists to focus on design and exploration. This approach represents a significant step towards automated, certified-by-design scientific software synthesis, revolutionizing the landscape of scientific research and discovery.

Object serialization and deserialization are widely used for storing and preserving objects in files, memory, or database as well as for transporting them across machines, enabling remote interaction among processes and many more. This mechanism relies on reflection, a dynamic language that introduces serious challenges for static analyses. Current state-of-the-art call graph construction algorithms do not fully support object serialization/deserialization, i.e., they are unable to uncover the callback methods that are invoked when objects are serialized and deserialized. Since call graphs are a core data structure for multiple types of analysis (e.g., vulnerability detection), an appropriate analysis cannot be performed since the call graph does not capture hidden (vulnerable) paths that occur via callback methods. In this paper, we present Seneca, an approach for handling serialization with improved soundness in the context of call graph construction. Our approach relies on taint analysis and API modeling to construct sound call graphs. We evaluated our approach with respect to soundness, precision, performance, and usefulness in detecting untrusted object deserialization vulnerabilities. Our results show that Seneca can create sound call graphs with respect to serialization features. The resulting call graphs do not incur significant runtime overhead and were shown to be useful for performing identification of vulnerable paths caused by untrusted object deserialization.

To implement important quality attributes of software such as architectural security tactics, developers incorporate API of software frameworks, as building blocks, to avoid re-inventing the wheel and improve their productivity. However, this is a challenging and error-prone task, especially for novice programmers. Despite the advances in the field of API-based program synthesis, the state-of-the-art suffers from a twofold shortcoming when it comes to architectural tactic implementation tasks. First, the specification of the desired tactic must be explicitly expressed, which is out of the knowledge of such programmers. Second, these approaches synthesize a block of code and leave the task of breaking it down into smaller pieces, adding each piece to the proper location in the code, and establishing correct dependencies between each piece and its surrounding environment as well as the other pieces, to the programmer. To mitigate these challenges, we introduce IPSynth, a novel inter-procedural program synthesis approach that automatically learns the specification of the tactic, synthesizes the tactic as inter-related code snippets, and adds them to an existing code base. We extend our first-place award-winning extended abstract recognized at the 36th IEEE/ACM International Conference on Automated Software Engineering (ASE'21) research competition track. In this paper, we provide the details of the approach, present the results of the experimental evaluation of IPSynth, and analyses and insights for a more comprehensive exploration of the research topic. Moreover, we compare the results of our approach to one of the most powerful code generator tools, ChatGPT. Our results show that our approach can accurately locate corresponding spots in the program, synthesize needed code snippets, add them to the program, and outperform ChatGPT in inter-procedural tactic synthesis tasks.

Secure by Design has become the mainstream development approach ensuring that software systems are not vulnerable to cyberattacks. Architectural security controls need to be carefully monitored over the software development life cycle to avoid critical design flaws. Unfortunately, functional requirements usually get in the way of the security features, and the development team may not correctly address critical security requirements. Identifying tactic-related code pieces in a software project enables an efficient review of the security controls' implementation as well as a resilient software architecture. This paper enumerates a comprehensive list of commonly used security controls and creates a dataset for each one of them by pulling related and unrelated code snippets from the open API of the StackOverflow question and answer platform. It uses the state-of-the-art NLP technique Bidirectional Encoder Representations from Transformers (BERT) and the Tactic Detector from our prior work to show that code pieces that implement security controls could be identified with high confidence. The results show that our model trained on tactic-related and unrelated code snippets derived from StackOverflow is able to identify tactic-related code pieces with F-Measure values above 0.9.

Prior research has shown that public vulnerability systems such as US National Vulnerability Database (NVD) rely on a manual, time-consuming, and error-prone process which has led to inconsistencies and delays in releasing final vulnerability results. This work provides an approach to curate vulnerability reports in real-time and map textual vulnerability reports to machine readable structured vulnerability attribute data. Designed to support the time consuming human analysis done by vulnerability databases, the system leverages the Common Vulnerabilities and Exposures (CVE) list of vulnerabilities and the vulnerability attributes described by the National Institute of Standards and Technology (NIST) Vulnerability Description Ontology (VDO) framework. Our work uses Natural Language Processing (NLP), Machine Learning (ML) and novel Information Theoretical (IT) methods to provide automated techniques for near real-time publishing, and characterization of vulnerabilities using 28 attributes in 5 domains. Experiment results indicate that vulnerabilities can be evaluated up to 95 hours earlier than using manual methods, they can be characterized with F-Measure values over 0.9, and the proposed automated approach could save up to 47% of the time spent for CVE characterization.

This article focuses on supporting artificial intelligence (AI)/machine learning (ML) security workers. It presents AI/ML adversarial techniques, tools, and common knowledge (AI/ML ATT&CK) framework to enable AI/ML security workers to intuitively explore offensive and defensive tactics.

Although call graphs are crucial for inter-procedural analyses, it is challenging to statically compute them for programs with dynamic features. Prior work focused on supporting certain kinds of dynamic features, but serialization-related features are still not very well supported. Therefore, we introduce Salsa, an approach to complement existing points-to analysis with respect to serialization-related features to enhance the call graph’s soundness while not greatly affecting its precision. We evaluate Salsa’s soundness, precision, and performance using 9 programs from the Java Call graph Assessment & Test Suite (CATS) and 4 programs from the XCorpus dataset. We compared Salsa against off-the-shelf call graph construction algorithms available on Soot, Doop, WALA, and OPAL. Our experiments showed that Salsa improved call graphs’ soundness while not greatly affecting their precision. We also observed that Salsa did not incur an extra overhead on the underlying pointer analysis method.