Hey, I’m Alex Portlandyes, like the city! 👋

I’m a senior at Brown University studying computer science with a focus on systems and programming languages. I’m interested in building secure, highly-performant systems that don’t compromise on correctness, and I specifically enjoy working in Rust.

Most recently, I made the Kani Rust Verifier's compiler 4x faster while working at AWS, made Sesame's sandboxing system 6.5x faster, and built a high-performance VRP optimizer that swept the end-of-semester competition in Brown's graduate Prescriptive Analytics class. (all built in Rust 🦀)

You can reach me at [email protected].

Publications

Experience

Work

This summer, I worked at Amazon Web Services as part of the Automated Reasoning Group. Specifically I was working on the Kani Rust Verifier, which plugs into the Rust compiler, using formal reasoning and SAT solving to prove the safety and correctness of your Rust code.

My project was to improve the performance of Kani’s compiler by 10% over the summer. I hit that goal in my first week and kept going – adding codegen caching, thread pools, function stubbing and more. I also found 22 small engineering inefficiencies throughout the codebase that collectively delivered a 1.52x speedup!

In the end, I made our compiler 3.97x as fast (benchmarked on the Rust standard library), much to the excitement of our users! Kani is fully open source, so feel free to check out my final presentation or the full series of optimizations on GitHub!

Before that, I also worked for the State of Rhode Island’s Division of IT, and for my hometown’s chapter of the ARC, a non-profit that cares for folks with developmental disabilities.

Research

I’ve been doing research with Malte Schwarzkopf as part of Brown’s ETOS Group since my sophomore year.

I started by working on Sesame, a system for enforcing privacy policies in Rust web apps. I specifically developed our runtime sandboxing system, for running arbitrary code without leaking private data. But that strong guarantee initially came with a prohibitive >2x overhead. I built an algorithm for copying arbitrary Rust types into the sandbox ~500x faster than through existing serialization, and developed a method for safe multithreaded sandbox reuse that reduced the total overhead by 6.5x.

Our work was published at SOSP ’24 - one of the top systems conferences. Presenting at the poster session in Austin was incredible and reinforced my passion for systems research.

Now, I’m leading sniff-test, a collaboration with Will Crichton from the Cognitive Engineering Lab, focused on building a system that can use code annotations to automatically document and check essential code properties (e.g. UB-free, panic-free, non-blocking) for safety-critical applications. This work was partially born out of requests from contributors to Rust crates like zerocopy, so I’m excited to continue rapidly developing our prototype based on feedback from them!

Teaching

This fall is my third time being a teaching assistant for Brown’s flagship computer systems course. As a TA, I lead weekly sections of ~25 students, teaching them systems programming in C++ and Linux. I really focus on making complex systems concepts accessible and try to create an environment where students feel comfortable asking questions up until they inevitably get that satisfying “aha!” moment!

Last year, I hired & led a staff of 24 TAs to teach the course’s 200+ students as a head TA, and I’ll be head TA again this spring! I’ve also TA-ed our software security and exploitation course.