Publications
2025
- 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point ProcessesSean Lamont, Christian Walder, Amir Dezfouli, Paul Montague, and Michael NorrishNeurIPS, 2025
A key challenge in automated formal reasoning is the intractable search space, which grows exponentially with the depth of the proof. This branching is caused by the large number of candidate proof tactics which can be applied to a given goal. Nonetheless, many of these tactics are semantically similar or lead to an execution error, wasting valuable resources in both cases. We address the problem of effectively pruning this search, using only synthetic data generated from previous proof attempts. We first demonstrate that it is possible to generate semantically aware tactic representations which capture the effect on the proving environment, likelihood of success, and execution time. We then propose a novel filtering mechanism which leverages these representations to select semantically diverse and high quality tactics, using Determinantal Point Processes. Our approach, 3D- Prover, is designed to be general, and to augment any underlying tactic generator. We demonstrate the effectiveness of 3D-Prover on the miniF2F and LeanDojo benchmarks by augmenting popular open source proving LLMs. We show that our approach leads to an increase in the overall proof rate, as well as a significant improvement in the tactic success rate, execution time and diversity. We make our code available at https://github.com/sean-lamont/3D-Prover.
@article{lamont20243d, title = {3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes}, author = {Lamont, Sean and Walder, Christian and Dezfouli, Amir and Montague, Paul and Norrish, Michael}, journal = {NeurIPS}, year = {2025}, url = {https://github.com/sean-lamont/3D-Prover}, } - Enhancing Malware Fingerprinting through Analysis of Evasive TechniquesAlsharif Abuadbba, Sean Lamont, Ejaz Ahmed, Cody Christopher, Muhammad Ikram, Uday Tupakula, Daniel Coscia, Mohamed Ali Kaafar, and Surya NepalarXiv preprint arXiv:2503.06495, 2025
As malware detection methods become more advanced and widespread, malware authors respond by adopting more sophisticated evasion mechanisms. However, traditional file- level fingerprinting, such as those provided by cryptographic and fuzzy hashes, is often overlooked as a potential target of evasion. Small variants within binary components are commonly used in malware attacks to evade traditional fin- gerprinting, as confirmed by Microsoft’s discovery of the GoldMax variations in 2020 and 2021. Despite this, no large- scale empirical studies have investigated the limitations of traditional malware fingerprinting methods applied to actual samples obtained from the wild and how their effectiveness could be improved. This paper addresses these gaps by answering three key questions: (a) To what extent are file variants commonly used in malware samples? To answer this question, we con- duct an empirical study of a large-scale dataset of 4 million Windows Portable Executable (PE) files reports, 21 million sections, and 48 million resources, which we split chronolog- ically into four groups to validate our analysis. Our findings suggest a high prevalence of similarities in deeper parts of PE files between 70% to 80%, including similar APIs in Im- port Libraries and common executable sections. (b) What file variant evasive methods can be observed? To answer this question, we cluster files with high similarities in their Im- port Libraries and common executable sections and labelled these clusters “Resilient fingerprints” after validating their maliciousness ground truth through the Virustotal vendor labels. We then conduct a qualitative analysis across our four groups to identify the variant parts of the top resilient finger- prints. Our findings indicate that non-functional mutations - such as alterations in the number of sections, virtual size, virtual address, and section names - are being used exten- sively as primary evasive variant tactics. We also identify two executable sections of interest that are similar within each resilient fingerprint, which we call malicious sections (high entropy > 5) and camouflage sections (entropy = 0). (c) How can we use these identified characteristics to improve mal- ware fingerprinting? To answer this question, we proposed two novel approaches that enhance malware fingerprinting and enable the identification of resilient fingerprints. Using a large dataset of 4 million feeds from VirusTotal, our find- ings indicate a large potential improvement in fingerprinting, with more than 50% of malware being identified compared to 20% using traditional fingerprinting approaches.
@article{abuadbba2025enhancing, title = {Enhancing Malware Fingerprinting through Analysis of Evasive Techniques}, author = {Abuadbba, Alsharif and Lamont, Sean and Ahmed, Ejaz and Christopher, Cody and Ikram, Muhammad and Tupakula, Uday and Coscia, Daniel and Kaafar, Mohamed Ali and Nepal, Surya}, journal = {arXiv preprint arXiv:2503.06495}, year = {2025}, } - Facing the Challenge of Leveraging Untrained Humans in Malware AnalysisBenjamin Zi Hao Zhao, Hassan Jameel Asghar, Muhammad Ikram, Mohamed Ali Kaafar, Sean Lamont, and Daniel CosciaIn ICT Systems Security and Privacy Protection, 2025
Software binary analysis, tools and machine learning aid security analysts in interpreting data, by automated means that filter, prioritize, and arrange pertinent information for skilled analysts. In this work, we revisit cooperative human-machine teams and evaluate the possibility of enabling untrained humans to assist machines and skilled analysts in their analysis of software binaries. Specifically, we propose a pipeline to transform a complex input domain into facial images on which untrained individuals make similarity decisions. Our faces include realistic human, animal, artistic, and anime faces that preserve inherent distances between data points of the input domain. Our approach is evaluated through a human study, where untrained respondents with minimal training successfully flag machine misclassifications. The untrained human does not replace the machine or skilled analyst, instead, utilized in a triage setting, to identify samples without historical precedence, deferring the decision to the skilled analyst for deeper inspection.
@inproceedings{10.1007/978-3-031-92882-6_5, author = {Zhao, Benjamin Zi Hao and Asghar, Hassan Jameel and Ikram, Muhammad and Kaafar, Mohamed Ali and Lamont, Sean and Coscia, Daniel}, editor = {Nemec Zlatolas, Lili and Rannenberg, Kai and Welzer, Tatjana and Garcia-Alfaro, Joaquin}, title = {Facing the Challenge of Leveraging Untrained Humans in Malware Analysis}, booktitle = {ICT Systems Security and Privacy Protection}, year = {2025}, publisher = {Springer Nature Switzerland}, address = {Cham}, pages = {61--75}, isbn = {978-3-031-92882-6}, } - RINSER: Accurate API Prediction Using Masked Language ModelsMuhammad Ejaz Ahmed, Christopher Cody, Muhammad Ikram, Sean Lamont, Alsharif Abuadbba, Seyit Camtepe, Surya Nepal, and Muhammad Ali KaafararXiv preprint arXiv:2509.04887, 2025
Malware authors commonly use obfuscation to hide API identities in binary files, making analysis difficult and time-consuming for a human expert to understand the behavior and intent of the pro- gram. Automatic API prediction tools are necessary to efficiently analyze unknown binaries, facilitating rapid malware triage while reducing the workload on human analysts. In this paper, we present RINSER (AccuRate API predictioN using maSked languagE model leaRning), an automated framework for predicting Windows API (WinAPI) function names. RINSER introduces the novel concept of API codeprints, a set of API-relevant assembly instructions, and supports x86 PE binaries. RINSER relies on BERT’s masked lan- guage model (LM) to predict API names at scale, achieving 85.77% accuracy for normal binaries and 82.88% accuracy for stripped bi- naries. We evaluate RINSER on a large dataset of 4.7M API code- prints from 11,098 malware binaries, covering 4,123 unique Win- dows APIs, making it the largest publicly available dataset of this type. RINSER successfully discovered 65 obfuscated Windows APIs related to C2 communication, spying, and evasion in our dataset, which the commercial disassembler IDA failed to identify [2]. Fur- thermore, we compared RINSER against three state-of-the-art ap- proaches, showing over 20% higher prediction accuracy. We also demonstrated RINSER’s resilience to adversarial attacks, including instruction randomization and code displacement, with a perfor- mance drop of no more than 3%.
@article{ahmed2025rinser, title = {RINSER: Accurate API Prediction Using Masked Language Models}, author = {Ahmed, Muhammad Ejaz and Cody, Christopher and Ikram, Muhammad and Lamont, Sean and Abuadbba, Alsharif and Camtepe, Seyit and Nepal, Surya and Kaafar, Muhammad Ali}, journal = {arXiv preprint arXiv:2509.04887}, year = {2025}, }
2024
- BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-ProvingSean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, and Paul MontagueIn Proceedings of the AAAI Conference on Artificial Intelligence, 2024
Artificial Intelligence for Theorem Proving has given rise to a plethora of benchmarks and methodologies, particularly in Interactive Theorem Proving (ITP). Research in the area is fragmented, with a diverse set of approaches being spread across several ITP systems. This presents a significant chal- lenge to the comparison of methods, which are often complex and difficult to replicate. Addressing this, we present BAIT, a framework for fair and streamlined comparison of learning approaches in ITP. We demonstrate BAIT’s capabilities with an in-depth comparison, across several ITP benchmarks, of state-of-the-art architec- tures applied to the problem of formula embedding. We find that Structure Aware Transformers perform particularly well, improving on techniques associated with the original prob- lem sets. BAIT also allows us to assess the end-to-end prov- ing performance of systems built on interactive environments. This unified perspective reveals a novel end-to-end system that improves on prior work. We also provide a qualitative analysis, illustrating that improved performance is associated with more semantically-aware embeddings. By streamlining the implementation and comparison of Machine Learning al- gorithms in the ITP context, we anticipate BAIT will be a springboard for future research.
@inproceedings{lamont2024bait, title = {BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving}, author = {Lamont, Sean and Norrish, Michael and Dezfouli, Amir and Walder, Christian and Montague, Paul}, booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence}, volume = {38}, number = {9}, pages = {10607--10615}, year = {2024}, }
2023
- Use of cryptography in malware obfuscationHassan Jameel Asghar, Benjamin Zi Hao Zhao, Muhammad Ikram, Giang Nguyen, Dali Kaafar, Sean Lamont, and Daniel CosciaJournal of Computer Virology and Hacking Techniques, 2023
Malware authors often use cryptographic tools such as XOR encryption and block ciphers like AES to obfuscate part of the malware to evade detection. Use of cryptography may give the impression that these obfuscation techniques have some provable guarantees of success. In this paper, we take a closer look at the use of cryptographic tools to obfuscate malware. We first find that most techniques are easy to defeat (in principle), since the decryption algorithm and the key is shipped within the program. In order to clearly define an obfuscation technique’s potential to evade detection we propose a principled definition of malware obfuscation, and then categorize instances of malware obfuscation that use cryptographic tools into those which evade detection and those which are detectable. We find that schemes that are hard to de-obfuscate necessarily rely on a construct based on environmental keying. We also show that cryptographic notions of obfuscation, e.g., indistinghuishability and virtual black box obfuscation, may not guarantee evasion detection under our model. However, they can be used in conjunction with environmental keying to produce hard to de-obfuscate version of programs.
@article{asghar_use_2023, title = {Use of cryptography in malware obfuscation}, issn = {2263-8733}, url = {https://doi.org/10.1007/s11416-023-00504-y}, doi = {10.1007/s11416-023-00504-y}, urldate = {2024-01-23}, journal = {Journal of Computer Virology and Hacking Techniques}, author = {Asghar, Hassan Jameel and Zhao, Benjamin Zi Hao and Ikram, Muhammad and Nguyen, Giang and Kaafar, Dali and Lamont, Sean and Coscia, Daniel}, year = {2023}, keywords = {Cryptography, Environmental keying, Malware detection, Malware obfuscation}, }
2019
- Computer Assisted Composition in Continuous TimeChamin Hewa Koneputugodage, Rhys Healy, Sean Lamont, Ian Mallett, Matt Brown, Matt Walters, Ushini Attanayake, Libo Zhang, Roger T. Dean, Alexander Hunter, Charles Gretton, and Christian WalderarXiv preprint arXiv:1909.05030, 2019
We address the problem of combining sequence models of symbolic music with user defined constraints. For typical models this is non-trivial as only the conditional distribution of each symbol given the earlier symbols is available, while the constraints correspond to arbitrary times. Previously this has been addressed by assuming a discrete time model of fixed rhythm. We generalise to continuous time and arbitrary rhythm by introducing a simple, novel, and efficient particle filter scheme, applicable to general continuous time point processes. Extensive experimental evaluations demonstrate that in comparison with a more traditional beam search baseline, the particle filter exhibits superior statistical properties and yields more agreeable results in an extensive human listening test experiment.
@article{koneputugodage2019computer, title = {Computer Assisted Composition in Continuous Time}, author = {Koneputugodage, Chamin Hewa and Healy, Rhys and Lamont, Sean and Mallett, Ian and Brown, Matt and Walters, Matt and Attanayake, Ushini and Zhang, Libo and Dean, Roger T. and Hunter, Alexander and Gretton, Charles and Walder, Christian}, year = {2019}, journal = {arXiv preprint arXiv:1909.05030}, } - An End to End Machine Learning Model for Compositional DataSean Lamont, Christian Walder, and Cheng Soon OngHonours Thesis, 2019
Compositional Data Analysis (CoDA) is the study of data which can be interpreted as ratios or counts. Data of this type manifests in many forms, ranging from microbiome species counts to wealth distributions. Mathematically, compositional data is known to exist in a simplex. This prevents many standard analysis methods, which assume Euclidean geometry, from being applied. Dimensionality reduction through Principal Component Analysis (PCA) is once such method. There are instead approaches to dimensionality reduction which are faithful to this compositional structure. These methods have been shown to preserve structures within the original data which are distorted by PCA. This thesis investigates representations of compositional data, and how they in- fluence supervised learning. Although there are visual examples of how PCA does not preserve compositional structure, it is not certain how this representation influ- ences performance when applied to supervised learning. By the same token, we do not know whether mathematically justified methods can improve performance. We compare standard Euclidean representations to those given by Compositional Data Analysis (CoDA) in terms of how they impact subsequent supervised learning perfor- mance. Doing this on three microbiome datasets, we found a significant improvement in performance when supervised learning was preceded by the CoDA methods. Our main contribution is the introduction of a novel end-to-end Machine Learning model. This model constructs a representation as a function of both a reconstruction and supervised loss. When testing this model on a smaller subset of the same data, we found it to give representations which reveal more useful structures for supervised learning. In these cases, this model outperformed all baseline methods including the CoDA based algorithms. For large dimensions, this model does not perform as well, which we argue is due to the relatively small sample sizes. Our findings add to the growing body of literature which shows the importance of properly justified Compositional Data Analysis.
@article{lamont2019end, title = {An End to End Machine Learning Model for Compositional Data}, author = {Lamont, Sean and Walder, Christian and Ong, Cheng Soon}, year = {2019}, school = {The Australian National University}, journal = {Honours Thesis} }
2017
- Generalised Discount Functions applied to a Monte-Carlo AImu ImplementationSean Lamont, John Aslanides, Jan Leike, and Marcus HutterAutonomous Agents and Multiagent Systems, 2017
In recent years, work has been done to develop the theory of General Reinforcement Learning (GRL). However, there are few examples demonstrating the known results regarding generalised discounting. We have added to the GRL simulation platform AIXIjs the functionality to assign an agent arbitrary discount functions, and an environment which can be used to determine the effect of discounting on an agent’s policy. Using this, we investigate how geometric, hyperbolic and power discounting affect an informed agent in a simple MDP. We experimentally reproduce a number of theoretical results, and discuss some related subtleties. It was found that the agent’s behaviour followed what is expected theoretically, assuming appropriate parameters were chosen for the Monte-Carlo Tree Search (MCTS) planning algorithm.
@article{lamont2017generalised, title = {Generalised Discount Functions applied to a Monte-Carlo AImu Implementation}, author = {Lamont, Sean and Aslanides, John and Leike, Jan and Hutter, Marcus}, journal = {Autonomous Agents and Multiagent Systems}, pages = {1589-1591}, year = {2017}, url = {https://www.ifaamas.org/Proceedings/aamas2017/pdfs/p1589.pdf}, publisher = {International Foundation for Autonomous Agents and Multiagent Systems}, }