Welcome to the personal/professional homepage of Ilan Buzzetti the adoring husband of the lovely Angelica Li. As with all ineligible ex-bachelors he comports himself with dignity and good humour. He is in his 2nd year of doctoral studies at the University of Texas at Dallas, home to the feared Temoc and the revered Enarc, and is the grateful recipient of the NSF's creatively named CSGrad4US scholarship and is a member of UTD's esteemed Eugene McDermott Graduate Fellows Program.
This webpage is optimized for a download-now-read-later experience. The nav buttons use a minimal (non-zero) amount of javascript to hide and display the different webpages.
And now a word from the man himself...
Hello! And welcome to my homepage! This serves both personal and professional purposes, which I believe to be inseperable at the granularity of leaders. That is, the professional character of an organization is inseperable from the personal character of its leaders. I am a leader of the organization comprised exclusively of myself, thus it is important for professional relationships to get a sense of the leader's character, namely myself.
For potential personal relationships I think an idea of the person's profession is also relevant. A person's profession accounts for a large part of how they spend their time and mental effort. It shapes not only how they see the world, but which parts of the world they see. This latter aspect, in combination with their personal values, is critical for understanding their decisions and attitudes, and I think it is the foundation of what we conceive of as expertise.
I research formally verified binary hardening and vulnerability discovery and mitigation at the Software Languages Security Lab of the University of Texas at Dallas.
Among my proudest accomplishments is formally proving the functional correctness and safety properties of the strspn function from the musl C-library compiled for ARMv8. This work involved using our inhouse Coq framework, Picinae, to reason over a lifted version of the binary code without any reference to the source code (if any even exists). I am grateful to my labmate, Shreya Soman, for her indispensible help with the proof and especially with wrangling the complexity of the MapMaker invariant. You can see the Strspn diagram I made as a roadmap for this project below.
Tool / Skill | Resources |
---|---|
Assembly | OpenSecurityTraining.info has a course. You can also look at this reference manual for the ARMv8-M architecture to see what that's like :) |
Bash | I don't remember how I learned Bash, but this guide looks useful. Please note that learning Bash, and any language, is a marathon. You can't learn all of the fine details in your first sitting. It's an iterative process of learning and applying. |
Coq | The canonical and indispensible resource for learning Coq is Volumes I & II of Software Foundations. |
CLI Tools | I also don't remember how I learned CLI tools, but lukesmith's productivity videos (example) were a big inspiration. Recently, I found the Bandit wargame at overthewire.org to be a kind and joyful introduction to some linux and Cybersec fundamentals. |
Python | I recommend Automate The Boring Stuff , though note that Python is overkill for many things like text processing and file manipulation. A shell scripting language like bash is a more lightweight wrapper for the underlying cli tools that Python uses anyways. This inspiring video convinced me that programming fluency is a powerful aide to the powers of good. |
Computer Science | I think teachyourselfcs.com has a great teaching / learning philosophy and learning recommendations. Their public advice is free, and itself is useful. Some of their textbooks aren't freely available, and their paid bootcamps I cannot attest to. |
I am looking for interested and capable undergraduates to assist with a variety of projects to support and directly contribute to my research. The smaller projects are great for students that have developed skills but find themselves without a directed outlet to apply them. Sizeable projects will involve paid compensation; novel insights that spur research results will result in authorship credit in the relevant research publication. I am open to working with talented and mature high schoolers, but I will have to consult our legal department to see if there are any complications. You can see a list of projects and their basic requirements below.
Project Description | Skills Required / Developed |
---|---|
Restructure and add features to a Ghidra pcode to Picinae IL translator. | Python, Coq |
Design and create a CVE explorer app using an offline copy of the NVD. | HTML, CSS, Javascript, Bash, cli tools |
Create or polish an Assembly-to-CFG graph generator to produce graphs like the above. | Bash, cli tools, LLM integration (optional) |
Picinae IL representation optimization - essentially create compiler optimization passes. | Coq, compiler optimization |
Find new graph-query templates for finding possible software vulnerabiliites. | Binary exploitation, compilers, graph querying |
Develop and prove functional correctness specifications for libc functions. | Coq/Picinae, assembly, formal methods |
If you would like to work with me on any of these projects please follow these instructions.
On the other hand there's this SO guide on answering questions.
When I'm faced with an incomplete question (asked over email or some other asynchronous medium) my policy is: