home

Recent Posts

What I've Learned About Formal Methods In Half a Year

April 10, 2023 ❖ Tags: writeup, formal-verification, lean, alloy, lisp, scheme

I started working on my master's degree last September. The goal was to return to my workplace as a domain expert in formal methods – a topic I knew I was interested in, and yet something I knew practically nothing about. I partially attribute my lack of exposure to the lack of supervised learning opportunities (courses) at my undergraduate institution. Brown has an ample supply of teaching and research faculty who work in the field, though, so I've been taking advantage of that and soaking up as much knowledge as I can. I'm writing this to summarize what I've learned and done through my few months at grad school, and also to touch on what I have yet to learn because, as it turns out, three semesters is not nearly enough time to become a "domain expert" in anything. A beginning practitioner, perhaps, but I'm sure even that's an overly-generous characterization.

read more →

Pushing Haunt to Its Limits

December 12, 2022 ❖ Tags: writeup, programming, lisp, guile, scheme, webdev

When I started writing this article, I didn't mean to do anything more than describe a comment system I'd written in Guile. But as often happens when I write, I soon found myself disregarding that original scope and recording the history of every line of code I've written that's ever been run by a web server. I settled on allowing this to be an article about incorporating dynamic content into a Haunt site – a use-case that Haunt probably wasn't built to support, but which works surprisingly well due to Haunt configurations being ordinary Scheme programs.

read more →

I Love My PinePhone

August 26, 2022 ❖ Tags: writeup, programming, arm, rust, pinephone, alpine, postmarketos, emacs

For the past ten months, I've been using my PinePhone as a "daily driver." By which, I mean it's been in my pocket everywhere I go, and it's the device I use to make phone calls. Depending on your familiarity with the PinePhone (or the state of "Linux Phones" more generally) this statement is either delirious, or vapid (why should I care that you use a "smart" phone just like the rest of us?) Don't be mistaken: the PinePhone is usable as a little cellular-capable PDA, and it's in a league of its own. This article is my attempt to document my experiences and rationale for wanting to use one, as well as my thoughts on mobile Linux in general.

read more →

Rust on the Flipper Zero

July 05, 2022 ❖ Tags: writeup, rust, embedded, hardware, flipperzero

My Flipper Zero arrived in the mail a few weeks ago, ending a nearly two-year wait for its arrival. For the uninitiated, it's a "multi-tool device for geeks": a development board for radio, IR, and GPIO in a Tamagotchi-like form-factor. It combines the capability of the GoodWatch with the cuteness of the Pwnagotchi. Part of the appeal, to me, is the ability to hack on the free (as in freedom) firmware. As capable as it was out of the box, providing plenty of amusement when my brother and I took it for a spin through some parking garages, there are still features I'd like to add to it. The problem is that I've been too pampered by Rust as of late to want to do my firmware hacks in C.

read more →

A Good-Bye Letter To My Life-Long Companion

May 13, 2022 ❖ Tags: non-technical

Last night – Thursday, May 12th, 2022, at 22:17L – my cat was put to rest. I tend to avoid publishing anything non-technical to this website, but she deserves to be remembered, and this is the only place I can be confident my writing will last. She'd been with me through most of my life, always bringing me comfort when I was stressed, and keeping watch over me when I was sick. I owe this to her.

read more →

ret2emacs

April 14, 2022 ❖ Tags: writeup, capture-the-flag, emacs, binary-exploitation, heap-feng-shui

It's that time of year again where I take some time to reflect on UMass CTF. This is going to be shorter than last year's. I put out eight challenges, and I'm only going to be writing about one of them. Code, documentation, and write-ups for the others are available here.

read more →

Dollar Bin Reverse Engineering

December 24, 2021 ❖ Tags: writeup, hardware, reverse-engineering, tc32, radare2, java

The background for this project is a lesson in avoiding dishonest vendors. Two years ago, I was looking to purchase a smart watch with sleep tracking capabilities; I've always had difficulty sleeping and wanted a way of finally quantifying that difficulty. One of my requirements was the ability to pull data off of the watch without the use of proprietary software, so the only options I was seriously considering were those on Gadgetbridge's "supported devices" list. At the time, I was still in high school, and still awed by the affordability of consumer electronics on websites such as AliExpress (woefully unaware of the ethical implications of supporting a totalitarian state's economy). Moreover, I was somewhat capable of reading and writing 汉语, so the Xiaomi Mi Band 2 fit the bill. I took to Ebay to purchase one, finding a listing for 10.99 USD with free shipping. I ordered it, and things were okay. That is, until the package arrived.

read more →

UMass CTF 2021 Postmortem

April 19, 2021 ❖ Tags: writeup, capture-the-flag

This was the first year our capture-the-flag event, UMass CTF 2021, was open to the public. The competition started Friday, March 26th at 18:00 EDT, and ended Sunday, March 8th at the same time. By the end of the competition, we had 1991 registered users, belonging to 1160 registered teams. No teams were tied, we had just one unsolved challenge, and each of the "harder" challenges had just one or two solves.

read more →

UMass CTF 2020 - suckless Writeup

December 13, 2020 ❖ Tags: writeup, capture-the-flag, security, binary-exploitation, myrddin

Well, this is certainly overdue. It's the writeup for a challenge I authored for this year's UMass CTF, which ran from October 5th to October 12th. Yes, I'm late. But when you attend a university that tried very hard to squeeze the entire semester twelve weeks, you're going to deal with burnout and not nearly enough time to do things outside of your coursework. So I'm finally coming back to the challenge now that the semester's ended.

read more →

The Many Faces of an Undying Programming Language

July 20, 2020 ❖ Tags: opinion, programming, lisp, common-lisp, scheme

This is a post I've been meaning to write for a while now: one anecdotally comparing programming languages in the Lisp family. I consider myself to be a Lisp hacker. Perhaps that much was obvious from the letter λ adorning my website's header, a reference to the λ-calculus which inspired John McCarthy to design the first LISP [1]. Yet, "Lisp hacker" likely means little unless you, too, consider yourself to be a Lisp hacker. Calling yourself one seems carry some level of unstated meaning. Indeed, some identify with more specific groups. "Schemer," or "Guiler," or "Racketeer," or "Clojurist." But "Lisp Hackers" ⊇ "Schemers". There is commonality shared among all, or at least most, of these programming languages, and the Lisp hackers recognize and appreciate that commonality – the characteristics that make a programming language a Lisp. Homoiconic syntax, powerful metaprogramming facilities, and editor support that, in my opinion, is unparalleled. (Yes, I am alluding to GNU Emacs.) This article, however, is concerned with the differences. In it, I will be considering the specifics of each dialect, and whether or not those specifics make for a language I would want to use to develop a new piece of software.

read more →