Mathematics
Practical Proof Potential: Examining the Algorithm Verification Ability of the Software Assurance Workbench
In modern cryptography, effective encryption schemes are specified by mathematical algorithms, which can be proven to have desired properties. However, in order to use these algorithms they must be implemented in a machine-readable language; these implementations must then have their equivalence verified to be fully trusted. In the past such verification has been done via statistical sampling, a technique that is useful but still insufficient for implementations with rarely triggered cases.
In order to address this deficiency one may use symbolic evaluation, running circuit representations of the programs using symbols that verify all possible inputs instead of just sample values. This method is particularly well-suited to languages like Cryptol, a domain-specific cryptographic language that strongly adheres to the functional paradigm.
While functional languages are simpler to formally verify, the process can be extended to traditionally state-dependent languages using tools such as the Software Assurance Workbench (SAW). SAW has the ability to run scripts which use automated theorem provers to symbolically verify Cryptol code, Java Bytecode, and the LLVM bitcode that can be generated from a C file.
In order to investigate the potential limitations of SAW in this use, a test suite was written in C consisting of modifications to a simple function that represented a range of common inputs, mid-routine statements, and outputs. This suite was then evaluated, using the LLVM conversion, for completion and correctness of evaluation.
To further examine the efficiency of SAW when given longer functions, multiple differing C implementations of lightweight cryptographic algorithms such as SIMON and SPECK were analyzed for equivalence to reference implementations written in Cryptol. Various modifications were made in the implementations, inspired by techniques used in code obfuscation, to determine the ability of SAW to correctly evaluate obfuscated code and the relative resource cost incurred by analyzing obfuscated code.
How did you find out that you could do research in your field in the summer?
I had known that summer research in fields such as mathematics and computer science was possible since high school, and learned about what specific places I could work at by visiting the UMBC Undergraduate Research web pages.
How did you know that research at NIST was what you wanted to do?
I had known about the NIST SURF program since my high school days, and had heard many great things about working there. I had been hoping for years to get the chance to spend at least one summer there and find out firsthand if it was as great as I had heard, and this year I finally got that chance.
Did you apply to other places?
I applied to half a dozen different summer research programs, and NIST was the only one that accepted me. I should have applied to more, but underestimated the amount of time personal statements take and didn’t finish all of my intended applications in time.
Was the application difficult to do? Did you have help with this?
The application was straightforward to complete, but even with help writing a good personal statement was still a daunting task.
What was your summer research project?
My project was evaluating the capabilities and limitations of a certain software package when used to attempt verification of the fact that two different implementations of an algorithm are equivalent. Essentially I tried making any modifications I could think of to an implementation to try to break the evaluation scripts used by the package.
Who is your mentor for your research project?
My mentor was Mr. Lawrence Bassham of the Cryptographic Technology Group.
How much time do you put into this work?
Standard 40-hour workweek for 11 weeks.
Were you paid? Where did you live?
There was a stipend, and there was also housing provided for out-of-area interns. I lived so close to the worksite that it was more convenient to just live at home, which made forming connections with the other interns a little bit more difficult.
What academic background did you have before you started?
I had taken almost all of the core math classes, of which the only one to actually be relevant was MATH 301 for the formal introduction to the concept of proof. I had also taken CMSC 202, which proved to be more useful than all of my other classes combined, if for no other reason than teaching me C++.
How did you learn what you needed to know for this project?
I already knew C++ and several basic programming concepts, such as data types, from CMSC 202, so there was almost no work necessary to pick up C and some of the memory-management concepts. My mentor also provided me with some relevant academic papers that covered certain concepts and certain algorithms that I used. Everything else I taught myself through a combination of trial-and-error and judicious use of web searches.
What was the hardest part about your research?
The hardest part about my research was putting together the presentation about it at the end. There were so many things that I tested and so many background areas that I needed to learn about that it was confusing trying to extract the immediately pertinent information and present it in a sensible format.
What was the most unexpected thing?
The most unexpected thing was the amount of freedom I was given. In college I always had certain exercises to do, certain chapters to read, certain tests to take and procedures to follow. At NIST I was more or less given free rein to figure out what needed doing and do it, as long as I was making progress towards getting my final results. I was not expecting to have so much leeway in making my own process.
How does this research relate to your course work?
The work with automated theorem provers gives another perspective to the proof process that is stressed in many upper level math classes, such as MATH 301. I am also minoring in Computer Science, and the work that I did to explore the steps in compiling code and reading a certain dialect of assembly are immediately relevant to lower-level classes like CMSC 313, which I am taking in the fall.
What is your advice to other students about getting involved in research?
Start early, talk to your professors, and take the time to learn what subfield you want to do research in. Deadlines come around sooner than you expect, and the letters of recommendation and personal statement about why you want to do certain research are more important than you might expect.
What are your career goals?
I’m not sure what I want to do as a career. I know that I hope to get a PhD in mathematics and either work with or do research in applied branches, but beyond that I don’t know yet.
8/25/2021
