Connecting to School WiFi With iwd

I’ve recently been going to campus more, which involved setting up WiFi again. Alas, since I have been on campus I have switched from wpa_supplicant to iwd and I believe the campus WiFi changed how authentication works as well. It’s often a little less obvious how to configure these enterprise WiFi networks on Linux, so hopefully this post will help point you in the right direction if you’re in a similar situation.


At the University of Pennsylvania the WiFi network for students is called “AirPennNet”. To connect we’ll need to create a /var/lib/iwd/AirPennNet.8021x file. This file should only be readable by root, as we’re going to put a password in it. The contents of this file are as follows:



We will use TTLS with tunneled PAP to authenticate, which basically sends the username and password over TLS to authenticate your connection to the network. In my case the username was simply the unique part of my e-mail address, and the password was my usual Penn password. You will likely have to change the EAP-Identity field to the one matching your institution.

Additionally we will need to add the /var/lib/iwd/airpennnet.cer file, which is the certificate used to verify that we are actually sending our username and password to the correct access point, and not just any router pretending to be AirPennNet.

I got the institution specific information and certificate from here:

And in particular this eventually led me to some general information about connecting to AirPennNet:

Hopefully this helps any weary Linux users at Penn get connected to the network.


Read more »

Return to Org

Refreshing my task management

Org mode has been a bit of a thorn in my side as of late. Yes, it’s true that I absolutely love org mode and it’s one of the few things keeping me from being a complete mess… But I have also never really made it work super well for task management for myself. In some sense, it has never had to be good at that for me to love it.

The fact of the matter is that org is not just one thing. It’s an incredible language for markup — beautifully more expressive than markdown, and far less finicky and verbose than LaTex. I use org-mode to take some notes, write some homework assignments and documentation, and even record recipes to make a cookbook. This is where org really shines for me. This is what I use it for.

But, org mode is also a huge (and hugely popular) task management system… I just don’t use it. So, let’s look at how we’re going to attempt to fix that… Yet again.

Read more »

What I Learned This Week: Subset types, real numbers, and more Coq


This has been a productive week with my Coqplexity project really starting to get off of the ground. Coqplexity is at the point now where it can automatically prove pretty much any polynomial Big O relation (as long as it’s true).

Some more work needs to be done in Coqplexity in order to make it more useful, but the foundation is there, and it’s been a good bit of experience in writing tactics and dealing with real numbers.

So, more stuff about subset types, tactics, and more!

Read more »

What I Learned This Week: Progress Sensitive Security, Erasure


Let’s keep this going! The goal of this is again, to write down some of my thoughts and what I did. This is not necessarily going to be accurate, but maybe it will be useful! Contact me if you find mistakes :).

The past week I have managed to get through another chunk of papers on the following topics:

  • Removing information leaks through the progress covert channel
  • Ensuring data erasure in programs which use untrusted data stores

Additionally, I have started to research real number libraries in Coq for use in a project…

Read more »

What I Learned This Week: Coinduction, Dependent Pattern Matching, and Langsec


I’m starting a small series. The gist of it? What I learned in the past week.

Each post will be a brief summary of some things which I studied in the past week. Not necessarily an in depth exploration of the topics, but you may find useful insight, or at least useful references if something is a topic of interest.

If you find a mistake in my understanding, or have a question, feel free to contact me!

With that out of the way, let’s talk about some of the things I read about this week. Coinduction in Coq, dependent pattern matching in Coq, and some papers in langsec.

Read more »

Absolutely Optimal

Program optimization is strange.

We naturally want our programs to run as quickly and efficiently as possible, but in some sense I have no idea what that actually means. Or, rather, I have no idea what “computation” actually entails.

Read more »

First Post!


I now apparently have a blog. I don’t know if this will ever see an update, or if this will ever be read by anybody, but the intention is to put some ramblings up here.

Read more »