Apple’s “Advanced Data Protection” feature for iCloud allows users to
keep most data stored in iCloud end-to-end encrypted such that even
Apple cannot access it. This is a great feature, but naturally a user
has to opt-in because it pushes the burden of data loss onto the user
themselves — if Apple cannot decrypt your iCloud photos, and you
lose your device which has access to the encryption keys for that
data, all of a sudden there is no way to get your photos back without
some serious breakthroughs in mathematics and computing. Bummer.
Fortunately, there are 2 recovery options that you can set up in case
you lose your device. One option is to generate a backup code, which
is essentially a complex password that will allow you to decrypt your
iCloud storage (presumably this code is used to encrypt a key that you
then give to Apple for safe keeping), and the other involves setting
up a “Recovery Contact” who will be able to help you recover your
account in case of disaster… But how does the recovery contact
feature actually work, and how safe is it to use?
Read more »
August 2, 2024 , Tags: iOS, cryptography, security, backups, encryption, iCloud
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, iwd, upenn, eduroam, airpennnet, penn
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