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.
AirPennNet
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:
[Security]
EAP-Method=TTLS
EAP-Identity=anonymous@upenn.edu
EAP-TTLS-Phase2-Method=Tunneled-PAP
EAP-TTLS-Phase2-Identity=<username>
EAP-TTLS-Phase2-Password=<password>
EAP-TTLS-CACert=/var/lib/iwd/airpennnet.cer
[Settings]
AutoConnect=true
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.
References
Read more »
June 9, 2024 , Tags: wifi, linux, upenn, eduroam
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 »
January 5, 2019 , Tags: emacs, org, org mode
WILTW #6
Hoof! Lots of papers, lots of writing!
Taking a peek into the Firefox verified crypto, and a bunch of Coq
libraries and frameworks.
Read more »
November 25, 2017 , Tags: wiltw, compcert, low*, hacl*, coq, tactics, fiat, bedrock, haskell
WILTW #5
This week has largely been administrative, with letters written, and
servers managed.
I went through the Tapir/LLVM paper, and had some thoughts about
theorem proving…
Read more »
November 18, 2017 , Tags: wiltw, llvm, tapir, coq, tactics
WILTW #4
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 »
November 12, 2017 , Tags: wiltw, coq, tactics, subset types, org, emacs
WILTW #3
This week more or less concludes my search for a real number library
in Coq, allowing me to get another project underway which needed
real numbers!
Additionally I have been messing a little bit more with subset
types, which should prove useful in the very near future.
Read more »
November 5, 2017 , Tags: wiltw, coq, subset types, org, emacs
WILTW #2
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 »
October 29, 2017 , Tags: wiltw, langsec, progress-sensitive, erasure, security, crypto, coq
Introduction
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 »
October 22, 2017 , Tags: coq, theorem proving, proofs, dependent types, pattern matching, wiltw, coinduction, langsec
I’m giving a talk as an introduction to dependently typed programming languages. The contents of this talk can be found in this post, and the slides can be found here.
Read more »
April 9, 2017 , Tags: haskell, idris, coq, formal verification, types, dependent types
I wrote a post about setting up Haskell development for ARM over on the Haskell Embedded blog that I’m a part of. You should check it out!
https://haskellembedded.github.io/posts/2015-12-15-arm.html
Read more »
December 16, 2015 , Tags: haskell, ARM, QEMU, Raspberry Pi
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 »
May 15, 2015 , Tags: compilers, optimization
Hello!
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 »
June 8, 2014 , Tags: misc