- 
+
diff --git a/src/components/PostList.astro b/src/components/PostList.astro
index f1e3db1..bca90e1 100644
--- a/src/components/PostList.astro
+++ b/src/components/PostList.astro
@@ -1,17 +1,31 @@
---
-import { getCollection } from "astro:content";
-const allPosts = await getCollection("posts");
+import { getCollection, type CollectionEntry } from "astro:content";
+import Timestamp from "./Timestamp.astro";
+import { sortBy } from "lodash-es";
+
+interface Props {
+ basePath: string;
+ includeDrafts?: boolean;
+}
+
+type Post = CollectionEntry<"posts">;
+const { basePath, includeDrafts } = Astro.props;
+const filter = includeDrafts ? (_: Post) => true : (post: Post) => !post.data.draft;
+const allPosts = await getCollection("posts", filter);
+const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
---
-
+
{
- allPosts.map((post) => {
+ sortedPosts.map((post) => {
return (
-
- | {post.data.date} |
+
+ |
+
+ |
-
+
{post.data.title}
@@ -21,3 +35,36 @@ const allPosts = await getCollection("posts");
})
}
|
+
+
diff --git a/src/components/Timestamp.astro b/src/components/Timestamp.astro
new file mode 100644
index 0000000..eab9889
--- /dev/null
+++ b/src/components/Timestamp.astro
@@ -0,0 +1,14 @@
+---
+interface Props {
+ timestamp: Date;
+}
+
+const { timestamp } = Astro.props;
+const datestamp = timestamp.toLocaleDateString(undefined, {
+ year: "numeric",
+ month: "short",
+ day: "numeric",
+});
+---
+
+{datestamp}
diff --git a/src/content/posts/2018-02-01-my-new-life-stack.md b/src/content/posts/2018-02-01-my-new-life-stack.md
new file mode 100644
index 0000000..0298da3
--- /dev/null
+++ b/src/content/posts/2018-02-01-my-new-life-stack.md
@@ -0,0 +1,56 @@
+---
+title: My new life stack
+date: 2018-02-01
+tags: ["arch", "linux", "setup", "computers"]
+---
+
+This is my first post on my new blog! I used to put a CTF challenge writeup here but decided to change it up a bit. Recently, I've been changing a lot of the technology that I use day to day. Here's some of the changes that I've made!
+
+## Operating System
+
+I've ran regular Ubuntu on my laptop for a while, then switched to Elementary OS, which I found a lot more pleasing to use. After using Elementary OS for about 6 months, some of the software on my computer started behaving strangely, and I decided it was time for some change.
+
+`````
+# michael @ arch in ~ [3:20:09]
+$ screenfetch
+ -`
+ .o+` michael@arch
+ `ooo/ OS: Arch Linux
+ `+oooo: Kernel: x86_64 Linux 4.14.15-1-ARCH
+ `+oooooo: Uptime: 6h 3m
+ -+oooooo+: Packages: 546
+ `/:-:++oooo+: Shell: zsh 5.4.2
+ `/++++/+++++++: Resolution: 1920x1080
+ `/++++++++++++++: WM: i3
+ `/+++ooooooooooooo/` CPU: Intel Core i7-6500U @ 4x 3.1GHz [37.0°C]
+ ./ooosssso++osssssso+` GPU: intel
+ .oossssso-````/ossssss+` RAM: 2963MiB / 7872MiB
+ -osssssso. :ssssssso.
+ :osssssss/ osssso+++.
+ /ossssssss/ +ssssooo/-
+ `/ossssso+/:- -:/+osssso+-
+ `+sso+:-` `.-/+oso:
+ `++:. `-/+/
+ .` `/
+
+`````
+
+I installed Arch Linux on my laptop the day before yesterday. I've used Arch Linux before, about a year ago, so setup was relatively familiar. On top of Arch Linux, I'm using the very widely recommended i3 tiling window manager, and urxvt terminal emulator.
+
+## Code Editor
+
+I usually use Sublime Text and Visual Studio Code (VSCode) equally much. Both editors are extremely customizable (and VSCode seems to be heavily inspired from Sublime), but when it comes down to it, VSCode doesn't outperform Sublime. There are many occasions when VSCode just takes forever (for example, when trying to open large codebases, and then automatically running static analyzers over the entire thing).
+
+Since I started using Arch Linux, I've been trying out neovim. I'm packing my configuration with plugins, and seeing how well it works out as my main code editor. If I get really comfortable with it, I'll share my init file on a Git repo, probably.
+
+## Browser... ??
+
+I used to use Chromium, and ..I still do. I've tried several alternatives, like Firefox or even Vivaldi, but all of them seem to be missing something. I haven't tried the new Firefox Quantum yet, but unless there's a really big reason for me to change my browser, I'm probably going to stick to Chrome for a while. Chrome's DevTools are by far the best I've used, and its general ease of use makes it my favorite browser.
+
+### cVim
+
+[cVim](https://chrome.google.com/webstore/detail/cvim/ihlenndgcmojhcghmfjfneahoeklbjjh?hl=en) is a nice Chrome extension that provides vim-like keyboard bindings to Chrome. I'm going to have to admit that there's a lot of quirks around using it on pages that have heavy key bindings, but ever since I started using it, I can't help but use j/k scrolling and H/L for back and forth navigation!
+
+## Personal Server
+
+I got a droplet off DigitalOcean for hosting things that I regularly depend on. In fact, this blog (running Ghost) is hosted there now! I'm also hosting a Git server over at [https://git.iptq.io](https://git.iptq.io). It's running Gitea, a Go-based GitHub alternative. This doesn't mean I'm completely ditching GitHub, I just have things that I _really_ want to keep private, private.
diff --git a/src/content/posts/2018-02-25-cleaning-up-your-shell.md b/src/content/posts/2018-02-25-cleaning-up-your-shell.md
new file mode 100644
index 0000000..8a8ce49
--- /dev/null
+++ b/src/content/posts/2018-02-25-cleaning-up-your-shell.md
@@ -0,0 +1,12 @@
+---
+title: "Cleaning up your shell"
+date: 2018-02-25
+tags: ["computers", "linux", "terminal"]
+languages: ["bash"]
+---
+
+Is your shell loading slower than it used to? Maybe you've been sticking a bit more into your `.bashrc`/`.zshrc` than you thought.
+
+It's only been a couple weeks since I installed my computer, and already my shell has been starting to lag. Since there's not that much I've put into my `.zshrc` file, I knew who the main culprits were. Namely, oh-my-zsh's "git" plugin and the nvm (node version manager) trying to load itself on startup. I'm not exactly in a situation where I need nvm most of the time I open my shell, so getting rid of that made my shell load a lot faster. It also means that every time I want to use node or npm, I'd have to manually call nvm, but that's not as important to me as a faster shell load time, especially since I don't really touch node that much.
+
+One trick you can use to see what scripts are being called at startup is the `-x` option (stands for xtrace) that popular shells like `bash` and `zsh` support. If you go into your shell and run `set -o xtrace`, you'll see it start to spit out some bash commands; this is the list of everything that is being run when your shell starts. You might find that some apps take a ridiculous amount of time to start up. These are some of the things you'd want to eliminate.
diff --git a/src/content/posts/2018-04-23-fixing-tmux-colors.md b/src/content/posts/2018-04-23-fixing-tmux-colors.md
new file mode 100644
index 0000000..47cbad1
--- /dev/null
+++ b/src/content/posts/2018-04-23-fixing-tmux-colors.md
@@ -0,0 +1,13 @@
+---
+title: "Fixing tmux colors"
+date: 2018-04-23
+tags: ["computers"]
+---
+
+Put this in your `~/.tmux.conf`.
+
+```bash
+set -g default-terminal "screen-256color"
+```
+
+If this isn't set properly, tmux usually assumes 16-color mode, which displays colors probably not like what you're used to.
diff --git a/src/content/posts/2018-05-28-web-apps.md b/src/content/posts/2018-05-28-web-apps.md
new file mode 100644
index 0000000..c13e659
--- /dev/null
+++ b/src/content/posts/2018-05-28-web-apps.md
@@ -0,0 +1,49 @@
+---
+title: "Web apps"
+date: 2018-05-28
+tags: ["computers", "web", "things-that-are-bad"]
+languages: ["javascript"]
+---
+
+The other day, I just turned off JavaScript from my browser. "fucking neckbeard", "you'll turn it back in 2 weeks", "living without JavaScript is like living without electricity" were some of the responses I got. And they might be right. But let's see why things are the way they are and what we can do about it.
+
+## What is the purpose of the web?
+
+Well, the answer's pretty obvious, right? So you can surf it. But what does that even mean anymore? In the past, surfing the web meant viewing websites. You'd open something like your favorite news website, and it'd show you some of the latest updates. Or maybe you'd open the website for some company to find out their telephone so you can contact them. In other words, it was a channel from which you could receive information.
+
+If you wanted to do anything more complicated or that required more interaction, like sending an email, you'd probably pop open a dedicated client to do it. Things like Microsoft Outlook, Mozilla Thunderbird serve as great email clients. For chat, you could use an IRC client. Hell, even the browser was a client, just for viewing webpages. If you didn't have a client for a service that you wanted to use, you'd download a client, enter in the details of the server you want to connect to, and then you would be off.
+
+Things aren't that way anymore. For some reason, the web browser has become the all-in-one client for every service. Instead of simply acting as a HTTP client, your browser is now also capable of running full-blown 3D games, chat rooms, real-time word processors, and [full x86 emulators, apparently](http://copy.sh/v86/). What the hell happened?
+
+## Spoiler alert: Javascript happened
+
+JavaScript happened. That little _scripting_ language invented to, you know, make some hover animation on your page or have dropdowns on your menu bar. Thanks to the introduction of JavaScript (and jQuery especially), developers stopped viewing webpages as Word documents that you can share, and more like canvases. Hover animations are cute and dropdowns are useful. Sure. But when this _scripting_ language starts turning into a _systems_ language (for lack of a better term), you have a problem. When's the last time you used Perl to write an operating system?
+
+Look at the things we do today with JavaScript. We have _full blown frameworks_ that we _compile_ into bundles of _executable code_ in people's browsers. We're basically talking about the equivalent of downloading a binary and executing it on your computer every time you open a _webpage_. Except for a few minor differences. Firstly, it's not really a binary, it's a huge blob of script, which means it must be executed inside some virtual interpreter. For each tab that you're running. Secondly, now you're downloading random scripts from any website that you open, and then [trusting it](https://superlogout.com/) and [running it][1]. You wouldn't hesitate to click a link, but you'd definitely think twice before installing something from an unknown source into your computer, right?
+
+On top of that, look at these huge frameworks that almost every company is hiring developers for: React, Angular, Vue. These frameworks help JavaScript developers develop "web apps", meaning your JavaScript is now responsible for things the browser should actually be doing for you: two-way data binding, template rendering, and more. Except now, you're downloading a script and running it inside of a virtual interpreter. And because of technologies like Webpack that bundles all your separate code files together (read: static linking), our browsers can't even use the same framework code from site to site.
+
+Look at Facebook's home page. Just from regular use, that webpage itself can use over 4 gigabytes of RAM. It makes large amounts of network calls for data that's all just being stored in memory. And everyone who opens the Facebook website (for the first time) must download _all_ of that JavaScript. The website has its own tabs (within the page, yes) for chat windows, games, advertisements, embedded video players, and much more I probably didn't even know about. Why are we running full-blown apps in our browser?
+
+## Ok but what can i do
+
+There's a number of things that can be done to turn this state of the web down a different path. Here's some ideas for users:
+
+- Disable JavaScript in your browser. Grant websites permission to use JavaScript only if they need it. You'd be surprised how many sites work with JavaScript disabled.
+- If you're not ready to do that yet or don't want to, consider [uBlock Origin](https://chrome.google.com/webstore/detail/ublock-origin/cjpalhdlnbpafiamejdnhcphjbkeiagm?hl=en). It's an extension that can block scripts by source.
+
+For developers:
+
+- [svelte](https://svelte.technology/) is a cool alternative to frameworks like Angular or React.
+- Consider the impact of every library you include. Can you do without it? What if you just wrote something from scratch instead of importing a full framework to do it?
+- Write more non-JavaScript software/libraries. Developers have only turned towards sticking JavaScript everywhere because it's easy to use, and libraries are readily available through npm.
+
+## Ok but what can you do
+
+I'm helping with a project called flubber, which originated as an IRC bouncer, but is slowly turning into a general messaging protocol. All-in-one messengers exist (and a particular one exists by that name exactly), but they all work by opening a browser view and just loading the page within it, so it's no different from just opening tabs in a browser. Flubber will communicate with these services through APIs, and then expose a uniform interface to clients which makes it easy to bring all into a single view. Check out my progress [here](https://github.com/iptq/flubber). Other than that, I'm also working on making my websites as light as possible in general, including this one which has no required Javascript (some pages use Katex for displaying math elements but are still readable without).
+
+And of course, I've disabled JavaScript in my browser.
+
+\ thanks for reading!
+
+[1]: https://web.archive.org/web/20190429040938/https://coinhive.com/
diff --git a/src/content/posts/2018-10-18-weechat-relay.md b/src/content/posts/2018-10-18-weechat-relay.md
new file mode 100644
index 0000000..f9ab10f
--- /dev/null
+++ b/src/content/posts/2018-10-18-weechat-relay.md
@@ -0,0 +1,85 @@
+---
+title: "Setting up IRC with Weechat"
+date: 2018-10-18
+tags: ["irc"]
+---
+
+I've just recently discovered that weechat has a "relay" mode, which means it can act as a relay server to other clients (for example, my phone). If I leave an instance of weechat running on, say, my server that's always running, it can act as a bouncer and my phone can receive notifications for highlights as well.
+
+The android app I'm using is called [Weechat-Android][2]. On my laptop I'm using [Glowing Bear][5].
+
+## Step 1: tmux
+
+To achieve this setup, first I install [tmux][1], which separates the terminal from the session. This means I can leave the weechat instance running in the background and detach my current session from it. The command for this is:
+
+```bash
+$ tmux new-session -s weechat
+```
+
+where the `-s` option just names the tmux session so it's not assigned some number.
+
+## Step 2: Add relay
+
+Now add a relay through weechat:
+
+```
+/relay add
+```
+
+where name is
+
+```
+[ipv4.][ipv6.][ssl.]name
+ ipv4: force use of IPv4
+ ipv6: force use of IPv6
+ ssl: enable SSL
+```
+
+according to the [documentation][3].
+
+## Step 2.5: SSL
+
+I'm using SSL on my relay endpoint, and I'd recommend anyone else to use it to. You could follow what the documentation says and generate a self-signed certificate, but getting a trusted certificate with [LetsEncrypt][4] is so easy there's almost no excuse not to do it.
+
+To start, install certbot, which is LetsEncrypt's handy bot that does everything for you. Once you're ready, run:
+
+```bash
+$ sudo certbot certonly
+```
+
+We want the `certonly` option because by default, certbot will try to install it into an existing HTTP server, but we're not using it for HTTP. This command should dump some files into `/etc/letsencrypt/live/`.
+
+Finally, just concatenate the important files, `privkey.pem` and `fullchain.pem` in that order, into `~/.weechat/ssl/relay.pem` (you can change that path with `/set relay.network.ssl_cert_key`). The file should look like:
+
+```
+-----BEGIN PRIVATE KEY-----
+...data...
+-----END PRIVATE KEY-----
+-----BEGIN CERTIFICATE-----
+...data...
+-----END CERTIFICATE-----
+```
+
+If your private key file starts with `BEGIN CERTIFICATE`, just change that to `BEGIN PRIVATE KEY` (change the END one too) and it should be fine.
+
+## Step 3: Set password
+
+Since weechat 1.6, the option to not use a password has been removed. So in order for clients to be able to connect to the server, you must set one using:
+
+```
+/set relay.network.password
+```
+
+The password should appear in asterisks in the weechat prompt box.
+
+## Step 4: Connect
+
+This depends on your setup, but you must make sure that your setup is reachable from the outside. Make sure the port that you chose for the relay is accessible through firewalls.
+
+That's it! If you're also using the android app to connect, just type in your host's address and password and you should be all good to go.
+
+[1]: https://wiki.archlinux.org/index.php/Tmux
+[2]: https://github.com/ubergeek42/weechat-android
+[3]: https://www.weechat.org/files/doc/stable/weechat_user.en.html#relay_commands
+[4]: https://letsencrypt.org/
+[5]: https://www.glowing-bear.org/
diff --git a/src/content/posts/2018-10-26-twenty-years-of-rsa-attacks.md b/src/content/posts/2018-10-26-twenty-years-of-rsa-attacks.md
new file mode 100644
index 0000000..5d149c3
--- /dev/null
+++ b/src/content/posts/2018-10-26-twenty-years-of-rsa-attacks.md
@@ -0,0 +1,244 @@
+---
+title: "Twenty years of attacks on rsa with examples"
+date: 2018-10-26
+toc: true
+tags: ["ctf", "crypto", "rsa"]
+languages: ["python"]
+math: true
+---
+
+There's [a great paper][1] I found by Dan Boneh from 1998 highlighting the
+weaknesses of the RSA cryptosystem. I found this paper to be a particularly
+enlightening read (and interestingly enough, it's been 20 years since that
+paper!), so here I'm going to reiterate some of the attacks described in the
+paper, but using examples with numbers in them.
+
+That being said, I _am_ going to skip over the primer of how the RSA
+cryptosystem works, since there's already a great number of resources on that.
+
+## Factoring large integers
+
+Obviously this is a pretty bruteforce-ish way to crack the cryptosystem, and
+probably won't work in time for you to see the result, but can still be
+considered an attack vector. This trick works by just factoring the modulus,
+$N$. With $N$, finding the private exponent $d$ from the public exponent $e$ is
+a piece of cake.
+
+Let's choose some small numbers to demonstrate this one (you can follow along in
+a Python REPL if you want):
+
+```py
+>>> N = 881653369
+>>> e = 17
+>>> c = 875978376
+```
+
+$N$ is clearly factorable in this case, and we can use resources like
+[msieve][7] or [factordb][2] to find smaller primes in this case. Since we know
+now that $N = 20717 \times 42557$, we can find the totient of $N$:
+
+```py
+>>> p = 20717
+>>> q = 42557
+>>> tot = (p - 1) * (q - 1)
+881590096
+```
+
+Now all that's left is to discover the private exponent and solve for the
+original message! (you can find the modular inverse function I used [here][3])
+
+```py
+>>> d = modinv(e, tot)
+51858241
+>>> pow(c, d, N)
+31337
+```
+
+And that's it! Now let's look at some more sophisticated attacks...
+
+## Elementary attacks
+
+These attacks are related to the _misuse_ of the RSA system. (if you can't tell,
+I'm mirroring the document structure of the original paper)
+
+### Common modulus
+
+My cryptography professor gave this example as well. Suppose there was a setup
+in which the modulus was reused, maybe for convenience (although I suppose with
+libraries today, it'd actually be more _inconvenient_ to reuse the key). Key
+pairs would be issued to different users and they would share public keys with
+each other and keep private keys to themselves.
+
+The problem here is if you have a key pair, and you got someone else's public
+key, you could easily derive the private key by just factoring the modulus.
+Let's see how this works with a real example now.
+
+Since this is a big problem if you were to really use this cryptosystem, I'll be
+using actual keys from an actual crypto library instead of the small numbers
+like in the first example to show that this works on 2048-bit RSA. The library
+is called [PyCrypto][4], and if you're planning on doing anything related to
+crypto with Python, it's a good tool to have with you. For now, I'm going to
+generate a 2048-bit key (by the way, in practice you probably shouldn't be using
+2048-bit keys anymore, I'm just trying to spare my computer here).
+
+```py
+>>> from Crypto.PublicKey import RSA
+>>> k1 = RSA.generate(2048)
+<_RSAobj @0x7f3d3226dfd0 n(2048),e,d,p,q,u,private>
+```
+
+Now, normally when you generate a new key, it'd generate a new modulus. For the
+sake of this common modulus attack, we'll force the new key to use the same
+modulus. This also means we'll have to choose an exponent $e$ other than the
+default choice of 65537 (see [this link][5] for documentation):
+
+```py
+>>> N = k1.p * k1.q
+29977270253913673973269594877868500604696844309480395834898813292056864035968758602074842333119394545818563664205865827843973433118231606201251719390934610989873635763197929136439794366715495587924829697045618064595517091398323127000591150167969423793125376862942962617933168868125721044755585292104012767604921511927694421931531763256179277376290836490302585046803170658011843375751827334637689505406974645481089358325805114205957009910758378725866614617688361814922628596814445370820099034880786971816556547138716303030977389113515312289367195090368607322922710704592536914377782096784092012774047931602714559411641
+>>> e = k1.e
+65537
+>>> d = k1.d
+15565200260470091881477501931717765645013182095721628848830000114674199708256113134107524142907363428287225581416015506594787249272629252596585055146773790032720599834991872233759704632573379913049026195290680640250863651116064783079834540016568221344526961094787464713454198443832494032866744158338151738236661515444305521301583312800890473043854752775780731961801793612989845832052044110301479536119434333369042172368546513808726742737729539432085793131998509039970952524552914892677427673231515899625998973161553704772256496315467235759715665448324408858980400807019213972046972829905566822336304711418843041721957
+>>> e2 = 65539
+>>> d2 = modinv(e2, (k1.p - 1) * (k1.q - 1))
+28155004966198083605557147846430301877082565365203402029588435163682086478799751838610856433805281302245406343554098644058282620662395619703047797297929171630352487059669029554823105971149580111303390225692229359101863845359614581890498607677708812792166993283364928728648227920436362454567967968010840963546889938282011875589987758165583590886451185216017928261116297436515322115306907044332595229241201447860504794919920665520170088035323466070517987985855014612353911537010064927051269052451478774966384895845225295261610911375622081716902881447610710645142912550905885899057916649884624811336671599114611316629599
+>>> k2 = RSA.construct((N, e2, d2))
+<_RSAobj @0x7f3d31c7c5f8 n(2048),e,d,p,q,u,private>
+```
+
+Ok, now we have two keys, $k_1$ and $k_2$. Now I'll show how using only the public
+and private key of $k_1$ (assuming this is the pair that we got legitimately from
+the crypto operator), and the public key of $k_2$, which is tied to the same
+modulus, we can find the private key of $k_2$.
+
+To do this, we'll try to find the roots of the equation:
+
+$$ f(x) = x^2 - (p + q)x + pq $$
+
+You'll find that for values of $p$ and $q$, this will produce $f(p) = p^2 - p^2
+\- qp + pq$, and $f(q) = q^2 - pq - q^2 + pq$. We know that $N = pq$. How can we
+find $p + q$? Since $\phi(N) = (p - 1)(q - 1) = pq - p - q + 1$, we can find
+that $\phi(N) = N - (p + q) + 1$, so $p + q = N - \phi(N) + 1$.
+
+Now we need to use $e$ and $d$ to estimate $\phi(N)$. Recall that $ed = 1 \mod
+\phi(N)$. This is equivalent to saying $ed = 1 + k\phi(N)$. Then $\frac{ed -
+1}{\phi(N)} = k$.
+
+It turns out that $k$ is extremely close to $\frac{ed}{N}$:
+
+$$ \frac{ed}{N} = \frac{1 + k\phi(N)}{N} = \frac{1}{N} + \frac{k\phi(N)}{N} $$
+
+$\frac{1}{N}$ is basically 0, and $\phi(N)$ is very close to $N$, so it
+shouldn't change the value of $k$ by very much. We now use $\frac{ed}{N}$ to
+estimate $k$:
+
+$$ \phi(N) = \frac{ed - 1}{\frac{ed}{N}} $$
+
+```py
+>>> from decimal import Decimal, getcontext
+>>> getcontext().prec = 1000
+>>> k = round(Decimal(e) * Decimal(d) / Decimal(N))
+34029
+>>> phi = (Decimal(e) * Decimal(d) - 1) / Decimal(k)
+Decimal('29977270253913673973269594877868500604696844309480395834898813292056864035968758602074842333119394545818563664205865827843973433118231606201251719390934610989873635763197929136439794366715495587924829697045618064595517091398323127000591150167969423793125376862942962617933168868125721044755585292104012767604575090001864613992237960887242026855773279634028088706121371418922552125986506064146112561599205615974813154971272528592745144988174228621487749404677959591894452249599588096076892574585613962026186332366180174253118634077603697727952204486962202338916762987146793208323561031870496718547544796269555861921652')
+```
+
+Then we can get $p + q$ through the formula mentioend above:
+
+```py
+>>> B = Decimal(N) - phi + 1
+Decimal('346421925829807939293802368937250520517556856274496340681799239089291249765321270491576943807769029506276203354532585613211864922584150104378865213010402223028176347214857274743206460295173009790370214772536128777858755035911614561414990603406404984005947717445743706054221064913595294226503135333158697489990')
+>>> C = Decimal(N)
+```
+
+Check to make sure $B$ and $C$ are integers. If they're not, try using a higher
+precision in `getcontext().prec`. Now solve the quadratic equation:
+
+```py
+>>> p = (B + (B * B - 4 * C).sqrt()) / Decimal(2)
+Decimal('178187650567807686297508761669341068026596182918164336679269778091413760248796912297951278062644499145975246732979455707116872915963269648808994075794761810506203681312867668286737214808081540392248516550834072470288052831951959306342657446325786002900014749794262752196461389552859745880480150585554246119623')
+>>> q = (B - (B * B - 4 * C).sqrt()) / Decimal(2)
+Decimal('168234275262000252996293607267909452490960673356332004002529460997877489516524358193625665745124530360300956621553129906094992006620880455569871137215640412521972665901989606456469245487091469398121698221702056307570702203959655255072333157080618981105932967651480953857759675360735548346022984747604451370367')
+>>> p * q == N
+True
+```
+
+We've successfully recovered $p$ and $q$ from just $N$, $e$, and $d$!
+
+### Blinding
+
+This attack is actually about RSA _signatures_ (which uses the opposite keys as
+encryption: private for signing and public for verifying), and shows how you can
+compute the signature of a message $M$ using the signature of a derived message
+$M'$.
+
+Suppose Marvin wants Bob to sign the following message: `"I (Bob) owes Marvin
+$100,000 USD"`. Marvin hands this to Bob saying something like, "I'll just need
+you to sign this with your private key." Let's generate Bob's private key:
+
+```py
+>>> from Crypto.Util.number import bytes_to_long, long_to_bytes
+>>> from Crypto.PublicKey import RSA
+>>> bob = RSA.generate(2048)
+<_RSAobj @0x7f4309521128 n(2048),e,d,p,q,u,private>
+>>> M = b"I (Bob) owes Marvin $100,000 USD"
+```
+
+Obviously, Bob, an intellectual, will refuse to sign the message. However,
+suppose Marvin now transforms his message into a more innocent looking one. He
+does this by turning $M$ into $M' = r^eM \mod N$ where r is an integer that's
+coprime to $N$:
+
+```py
+>>> from random import randint
+>>> N = bob.p * bob.q # this is publicly available knowledge
+>>> r = 19
+>>> Mp = long_to_bytes((pow(r, bob.e, N) * bytes_to_long(M)) % N)
+b'7\x90\xbc\xf9%T\xa9\xee\xf4\xe3?>]\x88\xcd\xb4\xd6D#\xfc\xcb\x0fd\xf0\x8e\xbc>\n\x06\xcd\x0f\x89\x0bp\xa7o\xd6\x02\xa6\xa7\x81\xd8\n\xae\xfb\x08\xaa|\xbd.\xc9E\xf1|\x86\xcaZ\xaa\xd4L\xafaA\x0c}\x84\x04\n\xa4\xa5\x80\xecX<\xe0\xb5\xf6\xfb\xe3\xcc\xd5BD7\xdc\xaep\x7f\xe9vi\xabB\xe2\xadE\xa41K\xc6\xb7\xae\x01\xcb\x04C\xaf\x8b\x17\x83\xffX7z\xb1\xbf\xceF\xafN(x\x00\x9f\xe1kV\xee\x0b\xbd\xc3H\r\xee9\x81\x16\xb2\x10hb.\x90\x08\xe42$Q\x92Ew+\xe1@\xf9\x17%\xce/\xbd\x00\xad\xe2\x12\x01\x93\x8b\xc4\x1bx\xe6H?\x15\xdfPE@\xf9j\xe3\xb7\x9e\xa0\x86\xd1\xd3\xb6[\xf7q\xf1\x95N\xd3>/\x06\x80\xc7\xa3\x8a\xcbDy\xc6v\x01P\x14\xa9Be\xf7~p\xc5\xaa\xac\xa0\xaf\xbe#\xe5\x18\xc6\x1d\xd5\x14\xc1\xbbYXD\x0c\x91{\xc0s\xde]\x18Z\x8bSk\x07k\xb6\x9a\xa5`Iqe~'
+```
+
+Now he asks Bob to sign this more... innocently-looking message. Without
+questioning, Bob, an intellectual, signs his life away. Let's say he produces a
+signature
+
+$$
+\begin{aligned}
+S' &= (M'^d) \\\
+&= (r^e * M)^d \\\
+&= r^{ed} * M^d \\\
+&= r * M^d \mod N
+\end{aligned}
+$$
+
+```py
+>>> Sp, = bob.sign(Mp, 0)
+4222298342813922437811434251340999736739055616654488323193778229765071846717137952694561809398626068283668428796351354154566771597532278827070832905206221261994843265685464173739776886856384806238418884247949451413559988796455422271296883338455956330421559319009950760931899199217936823999874162064553735563087382870564193673989865778229832918474778963380170967676966373703157629615331081637805594392084045827925764529711433584853942576464491576212176547485726609891593617931393545058401472883178443786988683045423150809606471425615670582973274971087459634959553685559458456237617436410759134193279063427911112115134
+```
+
+Now, all Marvin has to do is multiply by the modular inverse of $r$, to obtain
+$M^d$, the signature of the original message:
+
+```py
+>>> S = (Sp * modinv(r, N)) % N
+6137678992536399703654836416525985142902780822513172949427421060785532284955531529418529725602418902796840570634560123808769013384654624916503940938715718120521434666716675795201896105310462331838807171312705686415521871046533303776516500490921892398440988515777575520183847518597482163414665355222659603386541869176930658730416118799866012276767364050134126722746224706026850062367243018313483359694686773566231956425606553198607719740067340776177716443517567144901614253170719278035838849363127850910135864099535083004590180745762100334268408681888925040382341592080592207557742366581814701422371311084081150092871
+```
+
+Sure enough, if you try to verify the "original" signature against the original
+message, it checks out.
+
+```py
+>>> bob.verify(M, (S,))
+True
+```
+
+Marvin has now successfully tricked Bob into signing his life away.
+
+This post is a work in progress.. I'll update it as I add more.
+
+[1]: https://crypto.stanford.edu/~dabo/papers/RSA-survey.pdf
+[2]: http://factordb.com/
+[3]: https://stackoverflow.com/a/9758173
+[4]: https://github.com/dlitz/pycrypto
+[5]: https://www.dlitz.net/software/pycrypto/api/current/Crypto.PublicKey.RSA.RSAImplementation-class.html#construct
+[6]: https://crypto.stackexchange.com/a/14713
+[7]: https://github.com/radii/msieve
diff --git a/src/content/posts/2019-02-01-magic-forms-with-proc-macros.md b/src/content/posts/2019-02-01-magic-forms-with-proc-macros.md
new file mode 100644
index 0000000..29dc5a4
--- /dev/null
+++ b/src/content/posts/2019-02-01-magic-forms-with-proc-macros.md
@@ -0,0 +1,90 @@
+---
+title: "Magic forms with proc macros: Ideas"
+date: 2019-02-01
+tags: ["computers", "web"]
+languages: ["rust"]
+---
+
+Procedural macros (proc macros for short) in Rust are incredible because they allow arbitrary pre-compile source transformation, which leads to endless possibilities (and hazards!). But if we take careful advantage of this feature, we can use it to make clean abstractions for messy boilerplate, especially in the case of web forms.
+
+In fact, proc macros are incredibly pervasive around Rust's ecosystem. For example, using the [`serde`][1] serialization/deserialization crate, you can simply write:
+
+```rs
+#[derive(Serialize)]
+struct Foo {
+ bar: String,
+}
+```
+
+and code will be generated to serialize and deserialize to a multitude of formats including JSON, YAML, CBOR, etc.
+
+It occurred to me that this feature can also be useful for generating code for rendering and validating forms (as in a place where you fill out info). **wtforms** is one of the nicest Python packages for handling form behavior in web applications, and with the power of proc macros, this functionality can be easily achieved in Rust as well.
+
+In this post I'm going to outline some of the ideas I have for a wtforms-ish library for handling forms in Rust.
+
+## Code generation
+
+Ideally, we should be able to use this library like this:
+
+```rs
+#[derive(Form)]
+struct RegisterForm {
+ #[validators(email, custom("not_taken"))]
+ id: Email,
+ #[validators(required, length(4, 12))]
+ name: String,
+ #[validators(required, length(8, 128))]
+ pass: Password,
+}
+```
+
+What this would do is add a couple more functions to our form class. Firstly, I'd like to render an HTML version of the above form. Calling something like `RegisterForm::html()` should produce the following HTML (prettified here for convenience):
+
+```html
+
+```
+
+If we were to want to customize our form in any way, for example, adding more attributes to the elements, we would just attach that as a separate attribute onto the field:
+
+```rs
+#[validators(required, length(4, 12))]
+#[attrs = "autocomplete=off"]
+name: String,
+```
+
+This should generate the following HTML:
+
+```html
+
+```
+
+I realize this is probably not very flexible, since you'd really only be able to use this form in a specific context. But in reality, how much do you really lose by redefining that form?
+
+## Validation
+
+You've already seen the `validators` attribute used above. This defines a set of validators that we'd like to verify the form against. Suppose you receive an instance of the form that looks like (in pseudo-y Rust):
+
+```rs
+let instance = RegisterForm {
+ id: Email("michael@example.com"),
+ name: "michael",
+ pass: Password("pass"),
+}
+```
+
+then calling something like `instance.verify()` should run all those validators we've defined on the fields and return a list of errors that go along with each of the fields. For this instance, for example, we should at least get an error that states that the password provided was way too short.
+
+## Other interesting features
+
+- If a form fails during validation, the user is presented with the errors and a chance to retry the form. At this point, the HTML generated should fill in the values for the fields that passed the validation so the user doesn't have to fill it out again. You see this behavior on web forms sometimes.
+
+## Conclusion
+
+This project is a work in progress! You can see how far I am [on Github](https://github.com/iptq/wtforms).
+
+[1]: https://docs.rs/serde
diff --git a/src/content/posts/2019-03-04-server-analogy.md b/src/content/posts/2019-03-04-server-analogy.md
new file mode 100644
index 0000000..4c0a72c
--- /dev/null
+++ b/src/content/posts/2019-03-04-server-analogy.md
@@ -0,0 +1,20 @@
+---
+title: "Accept server analogy"
+date: 2019-03-04
+tags: ["computers"]
+---
+
+This is just a stupid analogy I thought of recently, but decided to write about it anyway.
+
+If you think about it, a server waiting for clients is kind of like the host at the front of a restaurant leading guests to tables. They don't actually take orders or serve food, they just stand at the front and wait for new guests to arrive. Then there's another waiter that's specifically assigned to take that table's orders.
+
+When a server binds to, for example, `localhost:3000`, what the server really gets is a file descriptor; this is what's meant by:
+
+```c
+int socket(int domain, int type, int protocol);
+int bind(int socket, const struct sockaddr *address, socklen_t address_len);
+```
+
+The `listen` library call then marks this socket as one that's open for connections, similar to marking the restaurant staff as a host rather than a waiter.
+
+According to the manpage for `accept`, when a connection-mode socket accepts a connection, it'll "extract the first connection on the queue of pending connections, create a new socket with the same socket type protocol and address family as the specified socket, and allocate a new file descriptor for that socket." This new socket would be the waiter who actually takes your orders.
diff --git a/src/content/posts/2020-04-01-password-managers.md b/src/content/posts/2020-04-01-password-managers.md
new file mode 100644
index 0000000..3ce63e3
--- /dev/null
+++ b/src/content/posts/2020-04-01-password-managers.md
@@ -0,0 +1,42 @@
+---
+title: "Password managers"
+date: 2020-04-01
+tags: ["computers", "things-that-are-good", "privacy"]
+---
+
+Password managers are programs that store passwords for you. With the number of accounts you keep on the web, you generally don't want to store all of them in your head. If you want to see articles on why you should use a password manager NOW, search "reasons to use a password manager" online and any of the articles you find should explain it. Here I'll add some more commentary on top of the traditional arguments.
+
+
+
+## Don't tick the "Remember master password box" no matter what
+
+How well you remember a password depends on how much you use it. If you open an account, make a password, and stay signed in for a year without ever having to re-login, you'll naturally forget the password. Same deal with password managers; the problem has just been moved another step.
+
+The power of a password manager comes from you continually entering in the same password over and over in order to unlock your other accounts.
+
+## Password managers are good for a lot more than passwords
+
+If you're willing to put sensitive passwords into your password manager, it should be a perfect place to put information that you'd want to avoid writing down in plaintext but want to access easily. This might include:
+
+- Backup / recovery codes
+- Your bank account number
+- Your car's license plate number
+- Answers to security questions, which leads into the next point:
+
+## Treat your security questions as passwords
+
+Save these in your password manager! "Security" questions are probably the worst idea for security and are more likely to weaken the security of your account than strengthen it. They have multiple fatal flaws (assuming you use security questions truthfully):
+
+- People can find out simple information about you through social engineering (favorite color, mother's maiden name, schools, etc.)
+- The answers to these questions aren't likely to change, and some can't be changed at will (in the case of a security problem, for example)
+- You probably won't even remember the exact format you typed in the answer, so if there's any fuzzy matching, it means the answers aren't hashed and salted to the same degree as passwords.
+
+Instead, just treat them as another password! Go into your password manager, generate the longest possible random password that fits into the box, and save it. Since you can give a name to the password, there's no worry of forgetting it or losing it, since it'll be stored among the vault of other passwords that you're hopefully using every day.
+
+## Don't trust extensions that fill in your password automatically
+
+Some password managers, like LastPass, have browser extensions that automatically fill in password boxes when you open the page.
+
+**Always turn this off, if possible. Prefer to look up the password and copy it in.**
+
+Once the extension copies the password into the page, it's fair game for any other JavaScript running on the page to grab your password. Not only that, there have been multiple reported vulnerabilities related to the LastPass extension mistakenly copying in a password because it couldn't correctly match the domain of the page to the domain of the password. Additionally, it doesn't work well if you have multiple passwords saved to the page, like if you have security questions saved to the page.
diff --git a/src/content/posts/2021-06-17-tracking-links.md b/src/content/posts/2021-06-17-tracking-links.md
new file mode 100644
index 0000000..be7ea62
--- /dev/null
+++ b/src/content/posts/2021-06-17-tracking-links.md
@@ -0,0 +1,101 @@
+---
+title: "Tracking links in email"
+date: 2021-06-17
+tags: ["email", "computers", "things-that-are-bad", "privacy"]
+---
+
+You probably get emails every day, and spend a lot of time reading them. And
+whenever someone performs an action or does something in vast quantities, you
+_bet_ the data giants have figured out a way to capitalize on it. For many
+years consumer privacy has basically gone unnoticed, and invasive tracking has
+grown [viral][1].
+
+Arguably, if you are someone who runs a business off of writing periodic
+newsletters that are distributed via email, you might want some statistics on
+how your newsletter is doing. Traditionally, this is achieved **actively**
+through some kind of survey with some kind of incentive, like "tell us how
+we're doing for a chance to win a water bottle".
+
+Now emails are typically imbued with **passive** trackers either in the form of
+[tracking pixels][3] (which informs the sender when the receipient opens the
+email) and [tracking links][4] (which informs the sender when AND what links
+receipients click). Tracking pixels are usually less relevant these days since
+many web-based email clients will ask before loading images, and clients run by
+mail servers with an enormous number of users like Gmail ([and soon iOS][5])
+may proxy the pixels ahead of time so the senders only see the IPs and metadata
+of the server.
+
+Tracking links, on the other hand, have become much more invasive, to the point
+where it's impossible to avoid being tracked. You see it all over the web:
+whenever you open a link, there's almost always some kind of `?ref=xxxxx` code
+stuck onto the end that identifies _your_ particular instance of it. This way,
+if you share the link with a friend, they just used the same code, and your
+connection to your friend is traced by the website owner.
+
+> If this creeps you out, consider using a browser extension like
+> [ClearURLs][6], which recognizes these URL parameters that do nothing but
+> feed information to the website owners and removes it for you.
+
+But email tracking links are even worse: they abuse redirects to obfuscate the
+original URL entirely. For instance, you'd get links in your email that look
+like:
+
+```
+https://some.mail.host/lWOrjb9FXYgMDS0DADOsxAZEFPB99gHzmRQTe6OHBws=
+```
+
+Where does it go? Wikipedia? Piratebay? There's only one way to find out: by
+making a request to that server, giving up information about the time, place,
+client, OS, and all sorts of other information that greedy data collection
+companies are waiting to snatch up.
+
+Of course, regular users notice nothing: these links are usually hidden behind
+buttons, text, or even the original URL itself. Once they click it, the website
+silently logs all the data it receives about the user, and then redirects the
+user to the original destination.
+
+The senders usually aren't at fault either. Sending email is tricky, with all
+the infrastructure set up to block out spam, so the majority of people who send
+bulk mail (newsletters, websites that need to confirm your email, etc.) all go
+through companies that handle this for them. Of course, being the middlemen who
+actually get the mail out the door, they're free to replace the links with
+whatever they want, and many of these companies advertise it as a feature to
+get more "insight" into how your emails are doing.
+
+Even worse, the original senders aren't the only ones getting the info, either.
+These middlemen could hold on to the data and there's no saying they can't use
+it for other purposes or sell it.
+
+Unfortunately, sending email isn't really going to get any easier, partly
+because of the way email fundamentally works: without all of the security
+infrastructure in place, running your own email server could easily lead to
+abuse. Most people (justifiably) would not go through all that effort
+themselves.
+
+Another possible avenue of thinking is to do what large mail companies did to
+oppose tracking pixels, where they would act as a mass-proxy for the links,
+opening them when they receive it, and transparently replace the unfiltered
+link back into the email so the user's device and location aren't revealed. But
+this raises its own issues: for example, what if the act of opening the
+original link performs some kind of action (e.g. click to subscribe, click to
+register, etc.)? Also, this solution only works for email that is not
+end-to-end encrypted. For end-to-end encrypted mail providers, there is no way
+to do this.
+
+The only real solution here is regulation via either advancement in
+privacy-related open standards or legislature. It's clear that without any kind
+of regulation, companies will continue to act in the interests of profit rather
+than the protection of their customers.
+
+> Devil's advocate afterthought: should this problem even be solved? Maybe
+> there's a benefit to this whole tracking thing. My opinion on this is if you
+> _really_ want to develop a community of readers, offer an easy way to give
+> feedback (or even go back to the incentive surveys), and if people aren't
+> giving feedback, then that itself is a reflection of the state of your
+> readers.
+
+[1]: https://www.wired.com/story/how-email-open-tracking-quietly-took-over-the-web/
+[3]: https://en.wikipedia.org/wiki/Web_beacon
+[4]: https://en.wikipedia.org/wiki/Click_tracking
+[5]: https://www.apple.com/newsroom/2021/06/apple-advances-its-privacy-leadership-with-ios-15-ipados-15-macos-monterey-and-watchos-8
+[6]: https://gitlab.com/KevinRoebert/ClearUrls
diff --git a/src/content/posts/2021-07-05-https-request-from-scratch.md b/src/content/posts/2021-07-05-https-request-from-scratch.md
new file mode 100644
index 0000000..54a380d
--- /dev/null
+++ b/src/content/posts/2021-07-05-https-request-from-scratch.md
@@ -0,0 +1,408 @@
+---
+title: "Sending https requests from scratch"
+date: 2021-07-05
+draft: true
+toc: true
+tags: ["computers", "web", "crypto"]
+languages: ["python"]
+---
+
+Every now and then, I return to this age-old question of _exactly_ how hard would it be to write a web browser from scratch? I hear some interviewers ask their candidates to describe the process your browser takes to actually put a webpage on your screen, but no doubt that's a simplification of a process from 20 years ago.
+
+Today, the specifications describing your browser's behavior [far exceeds 100 million words][4], and there's no sign of slowing. We are no longer just opening TCP sockets and sending `GET /path HTTP/1.0` anymore. That's why I decided to take some time and do some digging to see exactly how much it would take to send an HTTPS request from scratch, just like what the browser does, using as little existing tooling as I can.
+
+> **Disclaimer:** This is a experiment for demonstration purposes. Do **NOT** use this code for any real software.
+
+I'll be using Python for this since it's just for fun, the code will be pretty concise, and I don't have to write boilerplate outside of this post in order to make the code in it work. I'll try to stick to only using the Python 3 standard library as well, so not bringing in any external cryptography algorithms (the standard library provides `hashlib` tho). The downside here is the struct serialization and deserialization (using the [Python struct library][5]) gets a bit messy if you don't know how it works, but that information is all in the RFC anyway.
+
+**💡 This is a literate document.** I wrote a [small utility][3] to extract the code blocks out of markdown files, and it should produce working example for this file. If you have the utility, then running the following should get you a copy of all the Python code extracted from this blog post:
+
+```bash
+curl -o https.md -s {{< docUrl >}}
+markout -l py https.md > https.py
+```
+
+Otherwise, you can follow along and extract the code yourself as you read.
+
+With that out of the way, let's jump in!
+
+## URL Parsing
+
+This part is basically just a chore. URLs are defined in [RFC 3986][1], but we'll cheat a bit and just get the important parts we want for sending a request. First, I'll write out a regex for actually matching the parts we want:
+
+```py
+import re
+URL_PAT = re.compile(r"""
+ (?P[A-Za-z]+) # scheme (http, https,...)
+ :// # divider
+ (?P[A-Za-z\-\.]+) # hostname
+ (:(?P[0-9]+))? # port
+ (/ # divider
+ (?P[^?]*))? # path
+""", flags = re.VERBOSE)
+```
+
+We'll say if a string doesn't match this regex, then we won't count it as a URL. The rest of this part is just writing some glue code turning this regex into a dictionary:
+
+```py
+def parse_url(s: str):
+ m = URL_PAT.match(s)
+ if m is None: raise Exception("bad url")
+ return m.groupdict()
+u = parse_url("https://en.wikipedia.org")
+# {'scheme': 'https', 'host': 'en.wikipedia.org', 'port': None, 'path': None}
+```
+
+## TLS
+
+OK, now that we know where we're going to send the request, we should actually open a socket and talk to it. But before we want to send any data, we should _encrypt_ our communications. TLS is a protocol that conducts a brief handshake, then creates a tunnel where we can send data freely and it will be transparently encrypted before it goes over the wire. I haven't seen many example implementations of TLS out there (probably for a good reason), but without looking at actual code that works, it's hard to say I fully understand the protocol. So here I'll implement TLS 1.3 (defined in [RFC 8446][2]).
+
+- Worth noting here that TLS uses big-endian format for numbers.
+
+> **Second disclaimer:** hope I made it clear above but **THIS IS A TOY PROGRAM**. I'm about to roll my own crypto so do _not_ shove any of this code directly into a program if you value your safety. If you do plan on using this as a reference please get your code audited.
+
+### Record Layer
+
+TLS messages are sent in records, on top of TCP packets. This middle layer has its own header, described in section 5.1 of the RFC.
+
+Not a big deal, it just means we'll want a helper function to actually send our packets through this record over the socket. The implementation is short, and looks pretty much exactly like the definition:
+
+```py
+import struct
+def wrap_tls_record(ctype, rdata):
+ data = bytes()
+ data += struct.pack(">B", ctype) # content type encoded as a single byte
+ data += b"\x03\x03" # legacy_record_version, should just be 0x0303
+ data += struct.pack(">H", len(rdata)) # length of the data
+ data += rdata # finally, the record data itself
+ return data
+```
+
+### Handshake Layer
+
+But before we can send the first message, we also have to write some glue code for the handshake layer! This layer describes all handshake messages, and can be found in appendix B.3 of the RFC.
+
+Again, not too much code, just needs to be there. The annoying part of this is that the length is actually described with a `uint24`, which means it takes 3 bytes. Python's `struct` module doesn't actually have anything for this, so I'm just going to use the 4-byte unsigned option and chop off the first byte (remember, we are using big-endian encoding, so the MSB is the extra one).
+
+```py
+import struct
+def wrap_handshake(htype, hdata):
+ data = bytes()
+ data += struct.pack(">B", htype) # handshake type encoded as a byte
+ data += struct.pack(">I", len(hdata))[1:] # length, encoded as 3 bytes!
+ data += hdata # and then the handshake data
+ return data
+```
+
+### Client Hello
+
+TLS starts with the client sending a `ClientHello` message (defined in section 4.1.2 of the RFC), which basically starts the handshake off with some basic details about what the client can do. Now's probably a good time to decide on some basics, like which ciphers we'll be using to communicate.
+
+#### Cipher Suite
+
+In reality, encryption is mostly done at the hardware level, so browsers choose this based on what algorithms your hardware is fastest at. I pointed Firefox at Wikipedia and peeked into the connection details and it looks like I'm using AES-256-GCM with SHA-384, so I'll go with that. Let's see what byte sequence corresponds to these ciphers.
+
+```
+This specification defines the following cipher suites for use with
+TLS 1.3.
+
++------------------------------+-------------+
+| Description | Value |
++------------------------------+-------------+
+| TLS_AES_128_GCM_SHA256 | {0x13,0x01} |
+| TLS_AES_256_GCM_SHA384 | {0x13,0x02} | <-- this one
+| TLS_CHACHA20_POLY1305_SHA256 | {0x13,0x03} |
+| TLS_AES_128_CCM_SHA256 | {0x13,0x04} |
+| TLS_AES_128_CCM_8_SHA256 | {0x13,0x05} |
++------------------------------+-------------+
+```
+
+Cool, this means the two numbers `0x13` and `0x02` correspond to the cipher suite we want to use.
+
+#### Extensions
+
+Ridiculously enough, it seems that TLS 1.3 keeps a lot of pre-1.3 fields in there, renaming them `legacy_`, and then putting new features in extensions. This may help forward compatibility, but also means that some extensions end up not being extensions at all, but required components of the protocol. (I suppose this helps them phase out certain headers in later updates without changing the general layout)
+
+The extensions we'll need to support are listed in section 9.2 of the RFC. We'll only be sending the ones required during a `ClientHello`:
+
+- supported_versions (required)
+- signature_algorithms (required)
+- key_share (required)
+- server_name (required)
+- application_layer_protocol_negotiation
+
+What this means for our implementation is that for each of these we'll have to send a bit of information in the `ClientHello`. That's not too big of a deal; let's go through them one-by-one.
+
+(Before I start, I have to warn you; there are a LOT of length-wrappers. Most of these seem unnecessary since we're using Python, but I expect these were designed with generalization in mind)
+
+Supported versions is just what TLS 1.3 replaced the version header with; rather than saying up front that I want TLS 1.2, we have a general TLS framework for specifying extensions and then if I want to let the server know I can speak both TLS 1.2 and TLS 1.3, I'd put both versions into this extension.
+
+```py
+def ext_supported_versions():
+ versions = [b"\x03\x04"] # code number for TLS 1.3
+ versions = b"".join(map(lambda p: struct.pack(">B", len(p)) + p, versions))
+ return (struct.pack(">H", 43) # code number for supported_versions
+ + struct.pack(">H", len(versions))
+ + versions)
+```
+
+In TLS, clients have a pre-defined set of root authorities that it trusts, distributed by some trusted party like the OS or browser developers. These root authorities can then sign certificates for individual sites to prove to clients that they hold ownership over that domain. Clients can verify this proof cryptographically, using one of the signature algorithms we're going to to negotiate.
+
+For this I looked at some of the ciphers my browser supports, and just picked one that seems to have wide support: `ecdsa_secp256r1_sha256`.
+
+```py
+def ext_signature_algorithms():
+ algos = [b"\x04\x03"] # ecdsa_secp256r1_sha256
+ sig_algos = b"".join(algos)
+ ext = struct.pack(">H", len(sig_algos)) + sig_algos # yeah...
+ return (struct.pack(">H", 13) # code number for signature_algorithms
+ + struct.pack(">H", len(ext))
+ + ext)
+```
+
+Key negotiation is an important step, letting us establish a shared secret between the client and server without explicitly sending it over the network. Typically for this step, a form of Diffie-Hellman Exchange is performed, but pre-sharing a symmetric key is also used.
+
+Here we'll need to step a bit into the crypto. I'm going to choose elliptical-curve Diffie-Hellman ephemeral (ECDHE), which uses the elliptical curve operation to obscure keys as opposed to the original Diffie-Hellman which uses modular exponentiation. Cloudflare's blog has a [good introduction to elliptical curves][6].
+
+What this means for us is we need to pick parameters for initiating this exchange. First we'll pick a named group in the `supported_groups` extension, then we'll have to send the parameters for that particular group in the `key_share` extension. I'm going to pick secp256r1, the same algorithm as the one above, so I only need to implement one algorithm.
+
+supported_groups:
+
+```py
+def ext_supported_groups():
+ groups = [23] # secp256r1
+ groups = b"".join(map(lambda g: struct.pack(">H", g), groups))
+ ext = struct.pack(">H", len(groups)) + groups # yeah...
+ return (struct.pack(">H", 10) # code number for alpn
+ + struct.pack(">H", len(ext))
+ + ext)
+```
+
+key_share:
+
+```py
+def ext_key_share():
+ # hardcoding a fixed value here for now, we'll generate it later!
+ import binascii
+ x = b"\xf5\xddoi\xc8\x8c/#\x99\x8a\xaef\x8aWx\xacW,\xbad\x8d\x04\xac\x10\x05\xc2\x8f\x9bJ\x18\xf8."
+ y = b"\xfc}\x7f\xe0\x89\xb2YF\x0b\xc6\xb7\x00@\x04\xf6\x17Vl)V+\x18\xae\x157:o\xcc\x91\xf9\xaa#"
+ kex = b"\x04" + x + y
+ key_share = struct.pack(">H", 23) + struct.pack(">H", len(kex)) + kex
+ ext = struct.pack(">H", len(key_share)) + key_share
+ return (struct.pack(">H", 51) # code number for alpn
+ + struct.pack(">H", len(ext))
+ + ext)
+```
+
+Server name just lets the client tell the server what hostname it's expecting to connect to. The actual struct definitions here seem a bit over-the-top, but it's all in the name of future-proofing, right...?
+
+```py
+def ext_server_name(hostname: str):
+ sname = b"\x00" # code for hostname
+ sname += struct.pack(">H", len(hostname)) # length of hostname
+ sname += hostname.encode("utf-8")
+ ext = struct.pack(">H", len(sname)) + sname # yeah...
+ return (struct.pack(">H", 0) # code number for server_name
+ + struct.pack(">H", len(ext))
+ + ext)
+```
+
+Application layer protocol negotiation (ALPN) isn't technically required, but we'll put it there to force the server to send us HTTP2. The extension contents are just the list of names concatenated together.
+
+```py
+def ext_alpn():
+ protocols = [b"h2"] # http2, could also add http/1.1
+ alpn = b"".join(map(lambda p: struct.pack(">B", len(p)) + p, protocols))
+ ext = struct.pack(">H", len(alpn)) + alpn # yeah...
+ return (struct.pack(">H", 16) # code number for alpn
+ + struct.pack(">H", len(ext))
+ + ext)
+```
+
+Finally, let's combine all the functions above.
+
+```py
+def client_hello_extensions(hostname: str):
+ return b"".join([
+ ext_supported_versions(),
+ ext_signature_algorithms(),
+ ext_supported_groups(),
+ ext_key_share(),
+ ext_server_name(hostname),
+ ext_alpn(),
+ ])
+```
+
+Extensions is the last piece of information we need to create the entire `ClientHello` message. Soon we'll be able to get the server to respond to us!
+
+#### Putting the ClientHello message together
+
+```py
+import os
+def client_hello(hostname: str):
+ data = bytes()
+ data += struct.pack(">H", 0x0303) # legacy version
+ data += os.urandom(32) # 32 bytes nonce generated from /dev/urandom
+ data += b"\x00" # won't be using legacy_session_id, so send a zero
+ data += (b"\x00\x02" # we are sending 2 cipher suites
+ + b"\x13\x02") # the number for TLS_AES_256_GCM_SHA384
+ data += b"\x01\x00" # legacy_compression_methods
+
+ ext = client_hello_extensions(hostname)
+ data += struct.pack(">H", len(ext))
+ data += ext
+ return data
+```
+
+Let's send something to a server and see if that's what we want!
+
+```py
+import socket
+def test_client_hello():
+ hostname = "en.wikipedia.org"
+ s = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
+ s.connect((hostname, 443))
+
+ # send client hello
+ ch = wrap_tls_record(22, wrap_handshake(1, client_hello(hostname)))
+ s.send(ch)
+ return s.recv(1024)
+server_response = test_client_hello()
+# b'\x16\x03\x03...'
+assert server_response[0] == 0x16
+```
+
+If all went well, you should've received something with `\x16` as the first byte. That means the server sent a record with the content type `handshake(22)`. If you got `\x15`, it means you got an alert. In the next section we'll see how to interpret the server's response.
+
+### Server Hello
+
+The server hello is the response, where it tells us which ciphers and algorithms it chose, out of the ones we suggested. The code will look backwards from what we did above; instead of encoding a bunch of values, we'll read from what the server gives to us and interpret it instead.
+
+#### Change Cipher Spec
+
+Along with the Server Hello we'll also get a Change Cipher Spec record. According to the RFC, this is only in there for compatibility purposes, so we can safely ignore the one sent to us, but we'll also have to send a dummy Change Cipher Spec record as well.
+
+```py
+def change_cipher_spec():
+ return (b"\x14" # code number for change cipher spec
+ + b"\x03\x03" # legacy protocol version
+ + struct.pack(">H", 1) # length of change cipher spec message
+ + b"\x01")
+```
+
+Piece of cake.
+
+### Crypto
+
+> This is the deep-dive into the cryptographic portions of the protocol. If you're not too interested by this part, just continue on to the HTTP section.
+
+Let's walk through each of the ciphers and algorithms we're going to need one more time:
+
+- `ecdsa_secp256r1_sha256`
+ - ECDSA is the elliptical-curve signature algorithm; basically it can sign some information using the elliptical-curve private key, and anyone can verify using the corresponding public key that the person who owns the key has created that signature.
+ - secp256r1 just gives the name of a set of established parameters for a curve.
+ - SHA256 is a hashing algorithm, which creates a unique fingerprint of a piece of information that can't be reversed back to the original. Python's `hashlib` library provides this function for us, so we don't have to implement it ourselves.
+
+#### Naive Elliptical Curve Implementation
+
+#### secp256r1
+
+The curve is defined using the equation `y^2 = x^3 + ax + b mod p`.
+
+```py
+# https://hyperelliptic.org/EFD/g1p/auto-shortw.html
+
+```
+
+```py
+import secrets
+
+def ecdsa_keypair():
+ d = secrets.randbits(32)
+ Q = secp256r1.mul(secp256r1.G, d)
+ return (d, Q)
+
+(d1, Q1) = ecdsa_keypair()
+print("gen", d1, Q1)
+
+def ecdsa_sign(d, z):
+ while True:
+ # generate a number k between 1 and n-1
+ k = secrets.randbelow(secp256r1.n - 1)
+ if k == 0: continue
+
+ p = secp256r1.mul(secp256r1.G, k)
+ r = p.x % secp256r1.n
+ if r == 0: continue
+
+ s = (pow(k, -1, secp256r1.n) * (z + r * d)) % secp256r1.n
+ if s == 0: continue
+ break
+ return (r, s)
+
+(r1, s1) = ecdsa_sign(d1, 12345)
+print("sign", r1, s1)
+
+def ecdsa_verify(r, s, Q, z):
+ if not (r >= 1 and r < secp256r1.n and s >= 1 and s < secp256r1.n):
+ return False
+ sinv = pow(s, -1, secp256r1.n)
+ u1 = (z * sinv) % secp256r1.n
+ u2 = (r * sinv) % secp256r1.n
+ p = secp256r1.add(secp256r1.mul(secp256r1.G, u1), secp256r1.mul(Q, u2))
+ print(r)
+ print(p.x % secp256r1.n)
+ if r != p.x % secp256r1.n: return False
+ return True
+
+res = ecdsa_verify(r1, s1, Q1, 12345)
+print("res", res)
+```
+
+### Encrypted tunnel
+
+Now we should be ready to communicate with the server through our encrypted tunnel. But we forgot to keep around our key negotiation parameters! How will we encrypt our communication? Let's go back and update these functions to let us keep the parameters, using the crypto functions we just defined.
+
+The key sharing function:
+
+```py
+def ext_key_share(Q):
+ kex = b"\x04" + Q.x + Q.y
+ key_share = struct.pack(">H", 23) + struct.pack(">H", len(kex)) + kex
+ ext = struct.pack(">H", len(key_share)) + key_share
+ return (struct.pack(">H", 51) # code number for alpn
+ + struct.pack(">H", len(ext))
+ + ext)
+```
+
+Finally, the new `client_hello_extensions`:
+
+```py
+def client_hello_extensions(hostname: str):
+ d, Q = ecdsa_keypair()
+ data = b"".join([
+ ext_supported_versions(),
+ ext_signature_algorithms(),
+ ext_supported_groups(),
+ ext_key_share(Q),
+ ext_server_name(hostname),
+ ext_alpn(),
+ ])
+ return (data, d, Q)
+```
+
+## HTTP 2
+
+## `request`-like API
+
+## Conclusion
+
+What did we learn? Don't do this shit yourself, it's not worth it. We'll probably be on HTTP3 within the next year. Just import `requests` and be done with it.
+
+[1]: https://datatracker.ietf.org/doc/html/rfc3986
+[2]: https://datatracker.ietf.org/doc/html/rfc8446
+[3]: https://git.mzhang.io/michael/markout
+[4]: https://drewdevault.com/2020/03/18/Reckless-limitless-scope.html
+[5]: https://docs.python.org/3/library/struct.html
+[6]: https://blog.cloudflare.com/a-relatively-easy-to-understand-primer-on-elliptic-curve-cryptography/
+[7]: https://datatracker.ietf.org/doc/html/rfc7748
diff --git a/src/content/posts/2021-10-31-e2e-encryption-useless-without-client-freedom.md b/src/content/posts/2021-10-31-e2e-encryption-useless-without-client-freedom.md
new file mode 100644
index 0000000..55a37e3
--- /dev/null
+++ b/src/content/posts/2021-10-31-e2e-encryption-useless-without-client-freedom.md
@@ -0,0 +1,209 @@
+---
+title: "End-to-end encryption is useless without client freedom"
+date: 2021-10-31
+tags: ["computers", "privacy"]
+---
+
+Today, many companies claim to provide "end-to-end encryption" of user data,
+whether it be text messages, saved pictures, or important documents. But what
+does this actually mean for your data? I'll explain what "non-end-to-end"
+encryption is, why end-to-end encryption is important, and also when it might
+be absolutely meaningless.
+
+> If you just want to read about end-to-end encryption, click [here][1].
+> Otherwise, I'll start the story all the way back to how computers talk to
+> each other.
+
+## A game of telephone in a noisy room
+
+Computer networks essentially operate like a bunch of people yelling at each
+other at a public gathering, where everyone is kind of hearing everyone else's
+messages, but only really paying attention to ones addressed to them. Let's say
+I wanted to grab some Chipotle with my roommate. I'd yell "HEY NATHAN, WANNA GET
+CHIPOTLE?" over this public network, where Nathan would see his name, identify
+it as a message that is intended for him, and then reply accordingly. Notably,
+everyone _else_ listening to the network also hears this, and knows that I'm
+itching to get some Mexican food.
+
+That's not even the worst part, because well... how does your computer connect
+to the internet? Your router hears your computer's message, and passes it
+through a series of middlemen, who all perform this broadcasting ritual through
+some local network, until it gets to wherever your computer wanted to talk to in
+the first place. But in order for the middlemen to pass on the message, they'd
+have to hear the message, so now my lunch has become a public gathering known to
+everyone who's heard or passed on the message.
+
+## Encryption saves the day
+
+That's where **encryption** comes in. Encryption lets me change the message to
+something that the middlemen and everyone else listening on the network can't
+understand, but the person that I actually wanted to send the message can turn
+it back into the original. This way, I can be sure no one except Nathan got the
+memo of where we were grabbing lunch.[^3]
+
+So the way encryption's being used here is known as _transport_ encryption,
+since I'm _sending_ a message somewhere. Transport encryption is standard
+practice now through a technology called **transport-layer security**, or TLS,
+which is used by almost everything that talks to the internet, your browser,
+your email client, your phone. If it's not using TLS, it should be considered
+insecure.
+
+If you're thinking ahead, you might be thinking that the other place encryption
+can be used is **encryption at rest**. This is for documents and pictures that
+need to sit somewhere in storage for a while but shouldn't be visible to
+everyone. Many businesses require that their employees' laptops use _full-disk_
+encryption, so their data doesn't get compromised.
+
+When you put these together, your data is actually pretty safe from prying
+hands. If I put some tax documents on Google Drive, it'll use _transport_
+encryption to make sure no one steals my identity while I'm sending it, and
+encryption _at rest_ to make sure someone breaking into Google won't be able to
+just pull the hard drive out and read the files off it.
+
+## Two halves don't equal a whole
+
+It turns out just putting together these two types of encryption isn't enough.
+There's someone else we haven't protected ourselves against in this case, which
+is the party responsible for decrypting the transported data and then
+re-encrypting it at rest. Google can read all the documents I upload to Drive
+after decrypting it from transit and before encrypting it to disk. Facebook can
+read all the messages I send to my friends after decrypting it from transit and
+before re-encrypting it to send to my friends.
+
+And this is a lot smaller of a problem than it was before! Companies usually
+have privacy policies to protect user data from being used against what they
+expect, and many industries have laws like [HIPAA][hipaa] and [FERPA][ferpa] to
+make sure the people handling your data don't leak it.
+
+But we don't have to just _trust_ them on that, because we already _know_ how
+to protect data from middlemen who are simply taking a message and sending it
+somewhere else unchanged, like the ISPs from our networks. We just need _more_
+encryption!
+
+**End-to-end encryption** is just encrypting the data in a way that the only
+parties allowed to read the data are the people it was intended for. Password
+manager services like 1Password and Bitwarden use end-to-end encryption so that
+they're not decrypting your passwords when you store them online, they're just
+storing the encrypted data as-is, and then handing it back to your device which
+then decrypts it offline. [Signal][signal] famously provides end-to-end
+encrypted chat, so that no one, not even the government[^1], will be able to
+read the messages you send if they're not the intended recipient.
+
+## It's still not enough {#not-enough}
+
+End-to-end encryption seems like it should be the end of the story, but if
+there's one thing that can undermine the encryption, it's the program that's
+actually performing the encryption. Cryptographic operations are usually handled
+by clients, but unless you want to sit there adding points on an elliptic curve
+in a finite field, that client is your device or your browser, not you.
+
+The big problem here is how do you know your device is actually performing the
+encryption? How do you know the apps on your phone are only sending the data it
+needs to send, and not a lot more? Traditionally, independent researchers or
+bounty hunters may reverse-engineer client software and discover that they
+didn't quite operate as advertised, but we can't just rely solely on people
+from reddit with too much time on their hands to uphold security.
+
+Imagine if Google Drive was actually a physical vault service and the website
+was just a person you would hand your valuables to to keep safe. They could say
+"we're keeping this in military-grade security," but unless you watched what
+they did, how do you know they didn't cheap out on you and just shove it under
+the mattress where hackers breaking in could just steal everything?
+
+Same applies to Apple's recent child protection system. Their [white
+paper][csam] goes in painstakingly great detail about how photos are protected
+by "multi-layer" encryption before it's able to be decrypted by Apple. But
+typical users are not allowed to pick apart your iPhone to make sure it's
+encrypting everything correctly, or that the perceptual hashing algorithm it
+uses to filter pictures isn't just trivially flagging everything for manual
+review.
+
+WhatsApp data is stored unencrypted to the running application in order to
+store a database of messages locally. Additionally, this database can be backed
+up to iCloud, and according to [WhatsApp themselves][whatsapp], that data is
+stored unencrypted, which means that it may benefit from _transport_ security
+and _encryption at rest_ independently, but ultimately the people moving data
+around are still able to read it.
+
+I've also seen discussion of undermining end-to-end encryption in a [ghost
+proposal][ghost], a method that abuses multi-party encryption to add in a
+"ghost" listener, which can be the company or the government or anyone else
+that the vendor chooses. In theory, this backdoor could be prevented by an
+open-sourced client that properly checks each recipient to make sure it's the
+expected person before encrypting the message and sending it.
+
+Given that end-to-end encryption solely exists because trusting companies that
+run services is insufficient, it's safe to say that trusting companies to make
+client software that act in the interest of their users is just as useless as
+trusting companies to make services that act in the interest of their users.
+
+## What can i do?
+
+Although inconvenient, trusting different vendors for different pieces of this
+technological assembly line is the best way to prevent it from becoming abused.
+Many software use **open protocols**, communication schemes that are agreed
+upon and freely available to everyone[^2]. Then, independent parties develop
+and maintain lots of different software that all speak the same protocol, so if
+you don't trust a particular service to have an app that doesn't encrypt its
+data properly, you can just choose to use a different one by someone who you
+trust more.
+
+**Email** is a famous case of this: if I sign up for an email account with
+Outlook, I don't have to use a proprietary Outlook client. I _could_ if I
+wanted, and I imagine that there may be some features that Microsoft has added
+specifically to the Outlook website and apps, but since they claim to conform to
+the _open_ email specifications, I can just choose to use a different one.
+
+On top of that, email is _federated_, which means that if I didn't like
+Outlook's services, I could switch to a different provider and _still_ be able
+to chat with people on Outlook, unlike many of today's siloed services where I
+can't just message people on Facebook if I only have an account on Twitter,
+since they don't talk to each other using the same protocol.
+
+[**Matrix**][matrix] is a new chat network that also follows in the same spirit
+as email, but also has the benefits of multi-party encryption. There are
+multiple apps and servers, and servers can federate with each other using an
+open protocol. I would strongly recommend people who are interested in privacy
+to consider it.
+
+## Conclusion
+
+Why care? This might just seem to be some superficial political concern by
+privacy advocates who warn of dangerous edge cases that only matter to people
+whose rights are being violated by some dystopian government. Well, to put it
+bluntly, that dystopia is now, and it's not just the government we should be
+afraid of, but tech megacorps who possibly have even more power.
+
+We live in a digital world, so it's important to know how it works and who's in
+control.
+
+[^1]:
+ Governments and other parties with enough computational resources may
+ still be able to undermine specific levels of security, or just [threaten you
+ personally][wrench] until they get what they want.
+
+[^2]:
+ Large corporations typically still have majority representation in the
+ committees that decide on the most impactful specifications, but these are
+ still made available to researchers who can analyze and critique it.
+
+[^3]:
+ Not exactly; encryption by default is not authenticated. That means while
+ the data is protected in transit, there's no guarantee that the recipient is
+ actually who they say they are. I know only the recipient received my message,
+ but I don't know for sure the recipient is Nathan. In practice, browsers use
+ [PKI][pki] infrastructure to solve this, which relies on a certificate chain
+ that is distributed by browser or operating system vendors.
+
+[1]: {{< ref "#not-enough" >}}
+
+[csam]: https://www.apple.com/child-safety/pdf/CSAM_Detection_Technical_Summary.pdf
+[ferpa]: https://en.wikipedia.org/wiki/Family_Educational_Rights_and_Privacy_Act
+[ghost]: https://www.internetsociety.org/wp-content/uploads/2020/03/Ghost-Protocol-Fact-Sheet.pdf
+[hipaa]: https://en.wikipedia.org/wiki/Health_Insurance_Portability_and_Accountability_Act
+[signal]: https://signal.org/
+[wrench]: https://xkcd.com/538/
+[matrix]: https://matrix.org/
+[whatsapp]: https://faq.whatsapp.com/iphone/chats/how-to-back-up-to-icloud
+[scuttlebutt]: https://scuttlebutt.nz/
+[pki]: https://en.wikipedia.org/wiki/Public_key_infrastructure
diff --git a/src/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md b/src/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md
new file mode 100644
index 0000000..e521d7c
--- /dev/null
+++ b/src/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md
@@ -0,0 +1,182 @@
+---
+title: "building a formal cek machine in agda"
+draft: true
+date: 2022-02-02
+tags: ["computer-science", "programming-languages", "formal-verification", "lambda-calculus"]
+languages: ["agda"]
+toc: true
+---
+
+
+
+Last semester, I took a course on reasoning about programming languages using
+Agda, a dependently typed meta-language. For the term project, we were to
+implement a simply-typed lambda calculus with several extensions, along with
+proofs of certain properties.
+
+My lambda calculus implemented `call/cc` on top of a CEK machine.
+
+
+ Why is this interesting?
+
+Reasoning about languages is one way of ensuring whole-program correctness.
+Building up these languages from foundations grounded in logic helps us
+achieve our goal with more rigor.
+
+As an example, suppose I wrote a function that takes a list of numbers and
+returns the maximum value. Mathematically speaking, this function would be
+_non-total_; an input consisting of an empty set would not produce reasonable
+output. If this were a library function I'd like to tell people who write code
+that uses this function "don't give me an empty list!"
+
+But just writing this in documentation isn't enough. What we'd really like is
+for a tool (like a compiler) to tell any developer who is trying to pass an
+empty list into our maximum function "You can't do that." Unfortunately, most
+of the popular languages being used today have no way of describing "a list
+that's not empty."
+
+We still have a way to prevent people from running into this problem, though
+it involves pushing the problem to runtime rather than compile time. The
+maximum function could return an "optional" maximum. Some languages'
+implementations of optional values force programmers to handle the "nothing"
+case, while others ignore it silently. But in the more optimistic case, even
+if the list was empty, the caller would have handled it and treated it
+accordingly.
+
+This isn't a pretty way to solve this problem. _Dependent types_ gives us
+tools to solve this problem in an elegant way, by giving the type system the
+ability to contain values. This also opens its own can of worms, but for
+questions about program correctness, it is more valuable than depending on
+catching problems at runtime.
+
+
+
+## Lambda calculus
+
+The lambda calculus is a mathematical structure for describing computation. At
+the most basic level, it defines a concept called a _term_. Everything that can
+be represented in a lambda calculus is some combination of terms. A term can
+have several constructors:
+
+- **Var.** This is just a variable, like `x` or `y`. During evaluation, a
+ variable can resolve to a value in the evaluation environment by name. If
+ the environment says `{ x = 5 }`, then evaluating `x` would result in 5.
+
+- **Abstraction, or lambda (λ).** An _abstraction_ is a term that describes some
+ other computation. From an algebraic perspective, it can be thought of as a
+ function with a single argument (i.e f(x) = 2x is an abstraction, although
+ it would be written `(λx.2x)`)
+
+- **Application.** Application is sort of the opposite of abstraction, exposing
+ the computation that was abstracted away. From an algebraic perspective,
+ this is just function application (i.e applying `f(x) = 2x` to 3 would
+ result in 2\*3. Note that only a simple substitution has been done and
+ further evaluation is required to reduce 2\*3)
+
+### Why?
+
+The reason it's set up this way is so we can reason about terms inductively. The
+idea is that because terms are just nested constructors, we can describe the
+behavior of any term by just defining the behavior of these 3 constructors.
+
+Interestingly, the lambda calculus is Turing-complete, so any computation can be
+reduced to those 3 constructs. I used numbers liberally in the examples above,
+but in a lambda calculus without numbers, you could define integers recursively
+like this:
+
+- Let `z` represent zero.
+- Let `s` represent a "successor", or increment function. `s(z)` represents 1,
+ `s(s(z))` represents 2, and so on.
+
+In lambda calculus terms, this would look like:
+
+- 0 = `λs.(λz.z)`
+- 1 = `λs.(λz.s(z))`
+- 2 = `λs.(λz.s(s(z)))`
+- 3 = `λs.(λz.s(s(s(z))))`
+
+In practice, many lambda calculus have a set of "base" values from which to
+build off, such as unit values, booleans, and natural numbers (having numbers in
+the language means we don't need the `s` and `z` dance to refer to them).
+
+### Turing completeness
+
+As I noted above, the lambda calculus is _Turing-complete_. One feature of
+Turing complete systems is that they have a (provably!) unsolvable "halting"
+problem. Most of the simple term shown above terminate predictably. But as an
+example of a term that doesn't halt, consider the _Y combinator_, an example of
+a fixed-point combinator:
+
+ Y = λf.(λx.f(x(x)))(λx.f(x(x)))
+
+If you tried calling Y on some term, you will find that evaluation will quickly
+expand infinitely. That makes sense given its purpose: to find a _fixed point_
+of whatever function you pass in.
+
+> As an example, the fixed-point of the function f(x) = sqrt(x) is 1. That's
+> because f(1) = 1. The Y combinator attempts to find the fixed point by simply
+> applying the function multiple times. In the untyped lambda calculus, this can
+> be used to implement simple (but possibly unbounded) recursion.
+
+Because there are terms that may not terminate, the untyped lambda calculus is
+not very useful for logical reasoning. Instead, we add some constraints on it
+that makes evaluation total, at the cost of losing Turing-completeness.
+
+### Simply-typed lambda calculus
+
+The simply-typed lambda calculus (STLC) adds types to every term. Types are
+crucial to any kind of static program analysis. Suppose I was trying to apply
+the term `5` to `6`. As humans we can look at that and instantly recognize that
+the evaluation would be invalid, yet under the untyped lambda calculus, it would
+be completely representable.
+
+To solve this in STLC, we make this term completely unrepresentable at all. To
+say you want to apply 5 to 6 would not be a legal STLC term. That's because all
+STLC terms are untyped lambda calculus terms accompanied by a _type_.
+
+This gives us more information about what's allowed before we run the
+evaluation. For example, numbers may have their own type `Nat` (for "natural
+number"), while functions have a special "arrow" type `_ -> _`, where the
+underscores represent other types. A function that takes a number and returns a
+boolean (like isEven) would have the type `Nat -> Bool`, while a function that
+takes a boolean and returns another boolean would be `Bool -> Bool`.
+
+With this, we have a framework for rejecting terms that would otherwise be legal
+in untyped lambda calculus, but would break when we tried to evaluate them. A
+function application would be able to require that the argument is the same type
+as what the function is expecting.
+
+A semi-formal definition for STLC terms would look something like this:
+
+- **Var.** Same as before, it's a variable that can be looked up in the
+ environment.
+
+- **Abstraction, or lambda (λ).** This is a function that carries three pieces
+ of information: (1) the name of the variable that its input will be
+ substituted for, (2) the _type_ of the input, and (3) the body in which the
+ substitution will happen.
+
+- **Application.** Same as before.
+
+It doesn't seem like much has changed. But all of a sudden, _every_ term has a
+type.
+
+- `5 :: Nat`
+- `λ(x:Nat).2x :: Nat -> Nat`
+- `isEven(3) :: (Nat -> Bool) · Nat = Bool`
+
+Notation: (`x :: T` means `x` has type `T`, and `f · x` means `f` applied to
+`x`)
+
+This also means that some values are now unrepresentable:
+
+- `isEven(λx.2x) :: (Nat -> Bool) · (Nat -> Nat)` doesn't work because the type
+ of `λx.2x :: Nat -> Nat` can't be used as an input for `isEven`, which is
+ expecting a `Nat`.
+
+We have a good foundation for writing programs now, but this by itself can't
+qualify as a system for computation.
+
+## CEK machine
+
+A CEK machine is responsible for evaluating a lambda calculus term.
diff --git a/src/content/posts/2022-02-07-cybergrabs-ctf-unbreakable/index.md b/src/content/posts/2022-02-07-cybergrabs-ctf-unbreakable/index.md
new file mode 100644
index 0000000..5cb1494
--- /dev/null
+++ b/src/content/posts/2022-02-07-cybergrabs-ctf-unbreakable/index.md
@@ -0,0 +1,284 @@
+---
+title: "The Cyber Grabs CTF: Unbr34k4bl3 (942)"
+date: 2022-02-02
+tags: ["ctf", "crypto", "rsa"]
+languages: ["python"]
+math: true
+toc: true
+---
+
+Crypto challenge Unbr34k4bl3 from the Cyber Grabs CTF.
+
+
+
+> No one can break my rsa encryption, prove me wrong !!
+>
+> Flag Format: `cybergrabs{}`
+>
+> Author: Mritunjya
+>
+> [output.txt] [source.py]
+
+[output.txt]: ./output.txt
+[source.py]: ./source.py
+
+Looking at the source code, this challenge looks like a typical RSA challenge at
+first, but there are some important differences to note:
+
+- $n = pqr$ (line 34). This is a twist but RSA strategies can easily be
+ extended to 3 prime components.
+- $p, q \equiv 3 \mod 4$ (line 19). This suggests that the cryptosystem is
+ actually a [Rabin cryptosystem][Rabin].
+- We're not given the public keys $e_1$ and $e_2$, but they are related through
+ $x$.
+
+## Finding $e_1$ and $e_2$
+
+We know that $e_1$ and $e_2$ are related through $x$, which is some even number
+greater than 2, but we're not given any of their real values. We're also given
+through an oddly-named `functor` function that:
+
+$$ 1 + e_1 + e_1^2 + \cdots + e_1^x = 1 + e_2 + e_2^2 $$
+
+Taking the entire equation $\mod e_1$ gives us:
+
+$$
+\begin{aligned}
+ 1 &\equiv 1 + e_2 + e_2^2 \mod e_1 \\\
+ 0 &\equiv e_2 + e_2^2 \\\
+ 0 &\equiv e_2(1 + e_2)
+\end{aligned}
+$$
+
+This means there are two possibilities: either $e_1 = e_2$ or $e_1$ is even
+(since we know $e_2$ is a prime). The first case isn't possible, because with $x
+\> 2$, the geometric series equation would not be satisfied. So it must be true
+that $\boxed{e_1 = 2}$, the only even prime.
+
+Applying geometric series expansion, $1 + e_2 + e_2^2 = 2^{x + 1} - 1$. We can
+rearrange this via the quadratic equation to $e_2 = \frac{-1 \pm \sqrt{1 - 4
+(2 - 2^{x + 1})}}{2}$. Trying out a few values we see that only $\boxed{x = 4}$
+and $\boxed{e_2 = 5}$ gives us a value that make $e_2$ prime.
+
+## Finding $p$ and $q$
+
+We're not actually given $p$ or $q$, but we are given $ip = p^{-1} \mod q$ and
+$iq = q^{-1} \mod p$. In order words:
+
+$$
+\begin{aligned}
+ p \times ip &\equiv 1 \mod q \\\
+ q \times iq &\equiv 1 \mod p
+\end{aligned}
+$$
+
+We can rewrite these equations without the mod by introducing variables $k_1$
+and $k_2$ to be arbitrary constants that we solve for later:
+
+$$
+\begin{aligned}
+ p \times ip &= 1 + k_1q \\\
+ q \times iq &= 1 + k_2p
+\end{aligned}
+$$
+
+We'll be trying to use these formulas to create a quadratic that we can use to
+eliminate $k_1$ and $k_2$. Multiplying these together gives:
+
+$$
+\begin{aligned}
+ (p \times ip)(q \times iq) &= (1 + k_1q)(1 + k_2p) \\\
+ pq \times ip \times iq &= 1 + k_1q + k_2p + k_1k_2pq
+\end{aligned}
+$$
+
+I grouped $p$ and $q$ together here because it's important to note that since we
+have $x$, we know $r$ and thus $pq = \frac{n}{r}$. This means that for purposes
+of solving the equation, $pq$ is a constant to us. This actually introduces an
+interesting structure on the right hand side, we can create 2 new variables:
+
+$$
+\begin{aligned}
+ \alpha &= k_1q \\\
+ \beta &= k_2p
+\end{aligned}
+$$
+
+Substituting this into our equation above we get:
+
+$$
+\begin{aligned}
+ pq \times ip \times iq &= 1 + \alpha + \beta + \alpha\beta
+\end{aligned}
+$$
+
+Recall from whatever algebra class you last took that $(x - x_0)(x - x_1) = x^2
+\- (x_0 + x_1)x + x_0x_1$. Since we have both $\alpha\beta$ and $(\alpha +
+\beta)$ in our equation, we can try to look for a way to isolate them in order
+to create our goal.
+
+$$
+\begin{aligned}
+ pq \times ip \times iq &= 1 + k_1q + k_2p + k_1k_2pq \\\
+ k_1k_2pq &= pq \times ip \times iq - 1 - k_1q - k_2p \\\
+ k_1k_2 &= ip \times iq - \frac{1}{pq} - \frac{k_1}{p} - \frac{k_2}{q}
+\end{aligned}
+$$
+
+$\frac{1}{pq}$ is basically $0$, and since $k_1$ and $k_2$ are both smaller than
+$p$ or $q$, then we'll approximate this using $k_1k_2 = ip \times iq - 1$. Now
+that $k_1k_2$ has become a constant, we can create the coefficients we need:
+
+$$
+\begin{aligned}
+ \alpha + \beta &= pq \times ip \times iq - 1 - k_1k_2pq \\\
+ \alpha\beta &= k_1k_2pq
+\end{aligned}
+$$
+
+$$
+\begin{aligned}
+ (x - \alpha)(x - \beta) &= 0 \\\
+ x^2 - (\alpha + \beta)x + \alpha\beta &= 0 \\\
+ x &= \frac{(\alpha+\beta) \pm \sqrt{(\alpha+\beta)^2 - 4\alpha\beta}}{2}
+\end{aligned}
+$$
+
+Putting this into Python, looks like:
+
+```py
+from decimal import Decimal
+getcontext().prec = 3000 # To get all digits
+
+k1k2 = ip * iq - 1
+alpha_times_beta = k1k2 * pq
+alpha_plus_beta = pq * ip * iq - 1 - k1k2 * pq
+
+def quadratic(b, c):
+ b, c = Decimal(b), Decimal(c)
+ disc = b ** 2 - 4 * c
+ return (-b + disc.sqrt()) / 2, (-b - disc.sqrt()) / 2
+
+alpha, beta = quadratic(-alpha_plus_beta, alpha_times_beta)
+```
+
+Now that we have $\alpha$ and $\beta$, we can try GCD'ing them against $pq$ to
+get $p$ and $q$:
+
+```py
+from math import gcd
+
+p = gcd(pq, int(alpha))
+q = gcd(pq, int(beta))
+assert p * q == pq # Success!
+```
+
+### Alternative method
+
+@sahuang used the [sympy] library to do this part instead, resulting in much
+less manual math. It's based on [this] proof from Math StackExchange that $p
+\cdot (p^{-1} \mod q) + q \cdot (q^{-1} \mod p) = pq + 1$.
+
+[sympy]: https://www.sympy.org
+[this]: https://math.stackexchange.com/a/1705450
+
+```py
+from sympy import *
+p,q = symbols("p q")
+eq1 = Eq(ip * p + iq * q - pq - 1, 0)
+eq2 = Eq(p * q, pq)
+sol = solve((eq1, eq2), (p, q))
+```
+
+## Decrypting the ciphertexts
+
+Now that we know $p$ and $q$, it's time to plug them back into the cryptosystem
+and get our plaintexts. $c_2$ is actually easier than $c_1$, because with $e_2 =
+5$ we can just find the modular inverse:
+
+```py
+phi = (p - 1) * (q - 1) * (r - 1)
+d2 = pow(e2, -1, phi)
+m2 = pow(c2, d2, n)
+print(long_to_bytes(m2))
+# ... The last part of the flag is: 8ut_num83r_sy5t3m_15_3v3n_m0r3_1nt3r35t1n6} ...
+```
+
+This trick won't work with $c_1$ however:
+
+```py
+d1 = pow(e1, -1, phi)
+# ValueError: base is not invertible for the given modulus
+```
+
+Because $\phi$ is even (it's the product of one less than 3 primes), there can't
+possibly be a $d_1$ such that $2 \cdot d_1 \equiv 1 \mod \phi$. According to
+[Wikipedia][Rabin], the decryption for a standard two-prime $n$ takes 3 steps:
+
+1. Compute the square root of $c \mod p$ and $c \mod q$:
+ - $m_p = c^{\frac{1}{4}(p + 1)} \mod p$
+ - $m_q = c^{\frac{1}{4}(q + 1)} \mod q$
+2. Use the extended Euclidean algorithm to find $y_p$ and $y_q$ such that $y_p
+ \cdot p + y_q \cdot q = 1$.
+3. Use the Chinese remainder theorem to find the roots of $c$ modulo $n$:
+ - $r_1 = (y_p \cdot p \cdot m_q + y_q \cdot q \cdot m_p) \mod n$
+ - $r_2 = n - r_1$
+ - $r_3 = (y_p \cdot p \cdot m_q - y_q \cdot q \cdot m_p) \mod n$
+ - $r_4 = n - r_3$
+4. The real message could be any $r_i$, but we don't know which.
+
+Converting this to work with $n = pqr$, it looks like:
+
+1. Compute the square root of $c \mod p$, $c \mod q$, and $c \mod r$:
+ - $m_p = c^{\frac{1}{4}(p + 1)} \mod p$
+ - $m_q = c^{\frac{1}{4}(q + 1)} \mod q$
+ - $m_r = c^{\frac{1}{4}(r + 1)} \mod r$
+2. Using the variable names from [AoPS][CRT]'s definition of CRT:
+ - For $k \in \\{ p, q, r \\}, b_k = \frac{n}{k}$.
+ - For $k \in \\{ p, q, r \\}, a_k \cdot b_k \equiv 1 \mod k$.
+3. Let $r = \displaystyle\sum_k^{\\{ p, q, r \\}} \pm (a_k \cdot b_k \cdot m_k) \mod n$.
+4. The real message could be any $r$, but we don't know which.
+
+[CRT]: https://artofproblemsolving.com/wiki/index.php/Chinese_Remainder_Theorem
+
+In code this looks like:
+
+```py
+# Step 1
+mp = pow(c1, (p + 1) // 4, p)
+mq = pow(c1, (q + 1) // 4, q)
+mr = pow(c1, (r + 1) // 4, r)
+
+# Step 2
+bp = n // p
+bq = n // q
+br = n // r
+ap = pow(bp, -1, p)
+aq = pow(bq, -1, q)
+ar = pow(br, -1, r)
+
+# Step 3
+from itertools import product
+for sp, sq, sr in product((-1, 1), repeat=3):
+ m = (sp * ap * bp * mp + sq * aq * bq * mq + sr * ar * br * mr) % n
+ m = long_to_bytes(m)
+
+ # Step 4
+ # We know that the real flag starts with `cybergrabs{`...
+ if b"cybergrabs" in m: print(m)
+
+# Congratulations, You found the first part of flag cybergrabs{r481n_cryp70sy5t3m_15_1nt3r35t1n6_ ...
+```
+
+The final flag, then, is:
+
+```
+cybergrabs{r481n_cryp70sy5t3m_15_1nt3r35t1n6_8ut_num83r_sy5t3m_15_3v3n_m0r3_1nt3r35t1n6}
+```
+
+🎉
+
+Big thanks to @10, @sahuang, and @thebishop in the Project Sekai discord for
+doing a lot of the heavy-lifting to solve this challenge.
+
+[Rabin]: https://en.wikipedia.org/wiki/Rabin_cryptosystem
diff --git a/src/content/posts/2022-02-07-cybergrabs-ctf-unbreakable/output.txt b/src/content/posts/2022-02-07-cybergrabs-ctf-unbreakable/output.txt
new file mode 100644
index 0000000..a658bd9
--- /dev/null
+++ b/src/content/posts/2022-02-07-cybergrabs-ctf-unbreakable/output.txt
@@ -0,0 +1,5 @@
+n:267362205744654830055585746250317245125479735269853713372687604676608285629127977574310510441358104169652444917329986129098240750401425257601282268733834091593200445244725460613298199140690597119199763970064359847666802255456013592631532853951273286284878230893809080250386646832110506402289378691079462364884899662707502858007857457806853302449695351229004051902617728418480990341155900565542195318206284041182555579388392863474548687784403795738945489219689610881075059037192656116884269582257788959555951074322245033492165406470004019896763472332962300128378758934128374039937693688718317737657946435827745981009467876838127075176808098467305627394472135213533754815713468369763665632168616054982745256773112537152292099369137072982289095951236065885648588670059655452986720063260146952425798150221407866669449837430999779776718047668562687216933053536759554900663226163021145439386115076821161003965334731127329486856711654741683760749336235855319144478194501034662638054193682000283319917096796971
+ip:65491313526527942082900846848440586365393305192439699810712229312474732937502934334921061033822729150056656630858908294464249602368303871630644420585085642204592189073314730233318796675949142968346807766087775542461078648703191450221286915401606901781524237580646760734493950360267230729125514156671619347616
+iq:97034409222811998555255396847918439343239825222504093225438959283117395075159811973044380473862026342866489725039905931430797650466599952795602909181290621103197493223080488468216279214006070950393096075839913101687588555346523517436421698916141195686143520143972735534402754157166545851899187305574703394138
+c1:103687839591259628532585171241634220321003599759860095236990117623065664975385083122971507015385215246948744078816596026772744294701233346732383214113445480056584639282712898073542520168025667980980057512174927564196375256682206601425714094930670415979638437119896258396784978194294581076901000507291277729888015413204446158926865037965291316577726275211006619643531704449499845352147547986667837681877488120093302675775792115380914560935989896453159186176952126083066619414338359303033325593504442257083571002878083287293828310810483726711816109297046925744157605591270761804522735216774801135342322479770391505911100485259078064775709124730966391629468398187269096529671187877954443617005248499140455160589093379715757808387108825458007733207099871941497372539249357162437077379731766825184301649010270921003130776410066972952756983157217280397531412843118202051922048479332111760976091302376602674590153876045380552746826056547929265785960676415919260117136285580971488670143947003566230254837742519
+c2:171159809874438596904787534111610260851529969068192878049771299710688449419966698428704180474774734112617652498954998301185232279153644173070897800123538474930545720934844727376637921072749901149514789723141795042182408704214998390482343965532559149095934231081729041402598776401575561653660624208366051273601230345754361771067242657825194926706328336322383296953817730346429591680463526267530372572332663327157636745578067246913529155120642276894180354494816411827468256127607558873938451944866168777913756913920336763454881108023708284527878322162463081091624350220308273550298342755582044860337692076513609120342318151660103532559583052954725303030103413034880155621982581677423267299780543045375467310718078800411397780269409147558121862038983169509828944551199620508493589091401498720419409158373805529997911655270528589050795214164221299581104149954423726171539700223299445034347915430838395255700425648686205603925507474877720680274914513203566997846945579395522000899007446797091893230195801607
diff --git a/src/content/posts/2022-02-07-cybergrabs-ctf-unbreakable/source.py b/src/content/posts/2022-02-07-cybergrabs-ctf-unbreakable/source.py
new file mode 100644
index 0000000..ee71306
--- /dev/null
+++ b/src/content/posts/2022-02-07-cybergrabs-ctf-unbreakable/source.py
@@ -0,0 +1,53 @@
+from Crypto.Util.number import *
+from secret import *
+
+
+assert (x>2 and x%2 == 0)
+assert (isPrime(e1) and isPrime(e2))
+
+def functor():
+ val1 , val2 = 0,0
+ for i in range(x+1):
+ val1 += pow(e1,i)
+ for j in range(3):
+ val2 += pow(e2,j)
+ assert (val1 == val2)
+
+def keygen():
+ while True:
+ p,q = [getStrongPrime(1024) for _ in range(2)]
+ if p%4==3 and q%4==3:
+ break
+
+ r = 2
+ while True:
+ r = r*x
+ if r.bit_length()>1024 and isPrime(r-1):
+ r = r-1
+ break
+
+ return p,q,r
+
+
+functor()
+p,q,r = keygen()
+n = p*q*r
+print(f"p:{p}")
+print(f"q:{q}")
+ip = inverse(p,q)
+iq = inverse(q,p)
+c1 = pow(bytes_to_long(flag[0:len(flag)//2].encode('utf-8')),e1,n)
+c2 = pow(bytes_to_long(flag[len(flag)//2:].encode('utf-8')),e2,n)
+print(f"n:{n}",f"ip:{ip}",f"iq:{iq}",f"c1:{c1}",f"c2:{c2}",sep="\n")
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/content/posts/2022-03-03-clangd-in-nix.md b/src/content/posts/2022-03-03-clangd-in-nix.md
new file mode 100644
index 0000000..6c6c754
--- /dev/null
+++ b/src/content/posts/2022-03-03-clangd-in-nix.md
@@ -0,0 +1,34 @@
+---
+title: "Clangd in Nix"
+date: 2022-03-03
+tags: ["nixos"]
+---
+
+I've been using [Nix][NixOS] a lot recently since it handles dependency
+management very cleanly, but one gripe that I've been having is that when I'm
+doing C/C++ development work using `nix develop`, all my dependencies are
+actually in the Nix store in `/nix`, so my [clangd] editor plugin won't be able
+to find them.
+
+Fortunately, clangd supports looking for a file called `compile_commands.json`,
+which describes the compilation commands used for each file, with absolute paths
+for all dependencies.
+
+For [CMake]-based projects, there's an option to dump this information
+automatically into the build directory, which I typically then symlink into my
+project's root directory for my editor to find and apply to my files. Here's the
+snippet:
+
+```cmake
+# Generate the `compile_commands.json` file.
+set(CMAKE_EXPORT_COMPILE_COMMANDS ON CACHE INTERNAL "")
+
+if(CMAKE_EXPORT_COMPILE_COMMANDS)
+ set(CMAKE_CXX_STANDARD_INCLUDE_DIRECTORIES
+ ${CMAKE_CXX_IMPLICIT_INCLUDE_DIRECTORIES})
+endif()
+```
+
+[NixOS]: https://nixos.org/
+[clangd]: https://clangd.llvm.org/
+[CMake]: https://cmake.org/
diff --git a/src/content/posts/2022-03-04-learn-by-implementing-elliptic-curve-crypto.md b/src/content/posts/2022-03-04-learn-by-implementing-elliptic-curve-crypto.md
new file mode 100644
index 0000000..9ae5bf4
--- /dev/null
+++ b/src/content/posts/2022-03-04-learn-by-implementing-elliptic-curve-crypto.md
@@ -0,0 +1,127 @@
+---
+title: "Learn by Implementing Elliptic Curve Crypto"
+date: 2022-03-04
+tags: ["crypto", "learn-by-implementing"]
+draft: true
+math: true
+toc: true
+---
+
+Good places to start (in terms of usefulness):
+
+- [A relatively easy to understand primer on elliptic curve cryptography][2] by Cloudflare
+- [Elliptic-curve cryptography][3] from Practical Cryptography
+- [Elliptic-curve cryptography][1] on Wikipedia
+- [Elliptic Curve Cryptography: a gentle introduction][4] by Andrea Corbellini
+
+[1]: https://en.wikipedia.org/wiki/Elliptic-curve_cryptography
+[2]: https://blog.cloudflare.com/a-relatively-easy-to-understand-primer-on-elliptic-curve-cryptography/
+[3]: https://cryptobook.nakov.com/asymmetric-key-ciphers/elliptic-curve-cryptography-ecc
+[4]: https://andrea.corbellini.name/2015/05/17/elliptic-curve-cryptography-a-gentle-introduction/
+
+I'm writing this post because there's a lot of good posts out there introducing
+the elliptic curve formula, but not many that continue with getting from there
+to actually encrypting and decrypting messages. Maybe this is a good thing for
+discouraging people from writing insecure ECC implementations and using them in
+production, but it's not great for understanding the algorithm.
+
+> **DISCLAIMER:** I'm not a cryptographer! This is not a cryptographically
+> secure implementation, only used to demonstrate how the algorithm works. Read
+> [the SafeCurves intro][4] for some of the attacks a custom ECC implementation
+> may overlook.
+
+[4]: https://safecurves.cr.yp.to/index.html
+
+## Basic Ideas
+
+ECC starts with the idea that starting with an elliptic curve formula like $y^2
+= x^3 + ax + b$ that operates over a finite field $\mathbb{F}_p$, and defining
+an addition operation over two points, you can form a cyclic structure where
+adding a point to itself some number of times gets you back where you started.
+
+The interesting thing about this cyclic structure is that given the starting
+point $G$, also called the **generator** and some number $n$, you can find the
+$n$th element of that cycle $n \times G$ really quickly (in $\log(n)$ time). But
+if you're only given $G$ and $n \times G$, you can't figure out what $n$ is
+unless you brute force every possible number $n$ could be.
+
+What cryptographers have done is develop several sets of curve parameters that
+are publicly known, that include $a$, $b$, and the generator point $G$. Then
+users of the curve will just pick some $n$ and publish $n \times G$, and because
+of the difficulty of the elliptic curve discrete logarithm problem, $n$ will
+remain secret.
+
+There's some constraints on the properties of the curve parameters and $G$, but
+I won't go too far into that here since the proven curves have satisfies all
+those constraints.
+
+Once we have the curve and a keypair, there's all sorts of different
+cryptographic schemes that we can now build on top of these foundations:
+
+- [Encryption]({{< ref "#encryption" >}})
+- [Signatures]({{< ref "#signatures" >}})
+- [Key exchange]({{< ref "#key-exchange" >}})
+
+## Implementation
+
+I'll be implementing this using [Go]. I chose it for the ability to define
+methods out of order and independently of their associated structs, as well as
+their built-in big-integers library. This is required for compiling the Go
+module:
+
+[Go]: https://go.dev/
+[Markout]: https://git.mzhang.io/michael/markout
+
+```go
+package elliptic
+import (
+ "math/big"
+)
+```
+
+> This is a [literate document][literate]. You can run this blog post using [Markout]:
+>
+> ```
+> TODO:
+> ```
+
+[literate]: https://en.wikipedia.org/wiki/Literate_programming
+
+### Math primitives
+
+```go
+type Point struct {
+ x *big.Int
+ y *big.Int
+ inf bool
+}
+```
+
+Addition on $P$ and $Q$ is defined by first finding the line $PQ$, determining
+the point $-R$ where it intersects the curve again, and then returning $R$. We
+can find the line $PQ$ by using high school geometry:
+
+$$
+\begin{aligned}
+ (y - y_0) = m(x - x_0)
+\end{aligned}
+$$
+
+```go
+func (A Point) Add(B Point) Point {
+ // Find the slope between points A and B.
+ slope := big.NewRat(A.y - B.y, A.x - B.x)
+ return Point{}
+}
+```
+
+## Cryptographic applications
+
+These are some of the cryptographic primitives you can build over the above
+implementation.
+
+### Encryption
+
+### Signatures
+
+### Key exchange
diff --git a/src/content/posts/2022-05-09-installing-nixos-on-encrypted-zfs.md b/src/content/posts/2022-05-09-installing-nixos-on-encrypted-zfs.md
new file mode 100644
index 0000000..e5a72eb
--- /dev/null
+++ b/src/content/posts/2022-05-09-installing-nixos-on-encrypted-zfs.md
@@ -0,0 +1,190 @@
+---
+title: "Installing NixOS on ZFS with encryption"
+date: 2022-05-09
+tags: ["nixos", "linux", "setup"]
+toc: true
+---
+
+I finally switched over to NixOS for my desktop, and here is my install process.
+
+ Annoyingly enough, the biggest non-declarative part of Nix is this
+
+initial setup phase, and I made several mistakes during the install process, so
+I'm documenting the process here so I can remember for next time.
+
+- CPU: AMD Ryzen 7 3700X
+- GPU: NVIDIA GeForce RTX 3080 Ti
+- RAM: 80GB
+- Storage:
+ - SSD1: 1TB Samsung SSD 860 (encrypted), which I'm migrating off of
+ - SSD2: 2TB Crucial MX500 (encrypted), which I'm migrating to
+ - HDD: 3TB HITACHI HUA72303 (unencrypted), which serves as storage for music
+ and games.
+
+I already have my [Nix flake][1] setup for my other machines, but of those only
+my server runs NixOS. Instead, all my other machines use Arch Linux with just
+the Nix package manager installed on top.
+
+[1]: https://git.sr.ht/~mzhang/flake
+
+## Installation Media
+
+Since I'm using two SSDs, I don't bother with flashing the installation media on
+a USB stick and rebooting into that. I can just use Nix to get the tools that I
+need:
+
+```
+nix shell nixpkgs#nixos-install-tools
+```
+
+This will get me scripts like `nixos-generate-config` and `nixos-install` which
+I'll need for my setup.
+
+## Disk Setup
+
+First, I identified my disks. This can be done using `ls -l /dev/disk/by-id` and
+identifying the one corresponding to your disk.
+
+```
+export SSD1=/dev/disk/by-id/ata-Samsung_SSD_860_EVO_1TB_[...]
+export SSD2=/dev/disk/by-id/ata-CT2000MX500SSD1_[...]
+export HDD=/dev/disk/by-id/ata-HITACHI_HUA723030ALA640_[...]
+```
+
+Then, using some of the other references out there, I carefully used `sgdisk` to
+construct the partition tables. I want to dual boot NixOS with Windows, so I'm
+purposefully leaving out around 40% of the disk for that partition. (Note: use
+`sgdisk -L` to get the IDs for the `-t` parameter)
+
+```
+# Zap the disk
+sgdisk --zap $SSD2
+
+# 1: Boot partition
+sgdisk -n1:1M:+512M -t1:ef00 $SSD2
+
+# 2: NixOS partition
+# Note: bf01 is "Solaris /usr & Mac ZFS"
+sgdisk -n2:0:+1000G -t2:bf01 $SSD2
+```
+
+We'll let Windows create its own partitions using its installer later.
+
+## ZFS Setup
+
+```
+zpool create \
+ -o ashift=12 `# 2^12 = 4096 sector size, note small o` \
+ -o autotrim=on \
+ -O acltype=posixacl `# needed for some things` \
+ -O atime=off `# turn off access time` \
+ -O mountpoint=none `# turn off automatic mounting` \
+ -O compression=lz4 `# sure, why not` \
+ -O xattr=sa \
+ -O encryption=aes-256-gcm `# disk encryption` \
+ -O keyformat=passphrase \
+ rpool $SSD2-part2
+```
+
+It'll prompt for the encryption passphrase now.
+
+```
+mkfs.vfat $SSD2-part1
+zfs create -o mountpoint=legacy rpool/nixos
+```
+
+Mount them:
+
+```
+export MNT=/mnt/nixos
+mount -t zfs rpool/nixos $MNT
+
+mkdir $MNT/boot
+mount $SSD2-part1 $MNT/boot
+```
+
+## NixOS Hardware Configuration
+
+```
+nixos-generate-config --root $MNT
+```
+
+This writes the default configuration along with the results of the hardware
+scan. Although it says not to edit the file, this scrapes all of my virtual
+network interfaces which I do _not_ want in my general config, so I'll trim it a
+bit. Edit the file with:
+
+```
+$EDITOR $MNT/etc/nixos/hardware-configuration.nix
+```
+
+For the `configuration.nix` file, the following needs to be added somewhere in
+the file in order to get ZFS to work:
+
+```
+{
+ boot.supportedFilesystems = [ "zfs" ];
+ networking.hostId = "<8 random hex digits>";
+
+}
+```
+
+Also I chose to use GRUB instead of systemd-boot, so replace the line enabling
+systemd-boot with:
+
+```
+{
+ boot.loader.grub.enable = true;
+ boot.loader.grub.efiSupport = true;
+ boot.loader.grub.device = "nodev";
+}
+```
+
+## Install NixOS
+
+At this point I copied this configuration into my flake, so I can use all the
+packages that I've previously set up, including home manager.
+
+Run
+
+```
+nixos-install --root $MNT --flake flake#attr
+```
+
+Done! Now unmount the file systems:
+
+```
+umount $MNT/boot
+umount $MNT
+```
+
+## Neofetch
+
+```
+ ▗▄▄▄ ▗▄▄▄▄ ▄▄▄▖ michael@nucleus
+ ▜███▙ ▜███▙ ▟███▛ ---------------
+ ▜███▙ ▜███▙▟███▛ OS: NixOS 22.11 (Raccoon) x86_64
+ ▜███▙ ▜██████▛ Host: ASUSTeK COMPUTER INC. TUF GAMING X570-PLUS (WI-FI)
+ ▟█████████████████▙ ▜████▛ ▟▙ Kernel: 5.15.53
+ ▟███████████████████▙ ▜███▙ ▟██▙ Uptime: 1 day, 3 hours, 12 mins
+ ▄▄▄▄▖ ▜███▙ ▟███▛ Packages: 1406 (nix-system), 816 (nix-user)
+ ▟███▛ ▜██▛ ▟███▛ Shell: zsh 5.9
+ ▟███▛ ▜▛ ▟███▛ Resolution: 3840x2160, 1080x1920, 1920x1080
+▟███████████▛ ▟██████████▙ WM: i3
+▜██████████▛ ▟███████████▛ Terminal: alacritty
+ ▟███▛ ▟▙ ▟███▛ CPU: AMD Ryzen 7 3700X (16) @ 3.600GHz
+ ▟███▛ ▟██▙ ▟███▛ GPU: NVIDIA GeForce RTX 3080 Ti
+ ▟███▛ ▜███▙ ▝▀▀▀▀ Memory: 51392MiB / 80352MiB
+ ▜██▛ ▜███▙ ▜██████████████████▛
+ ▜▛ ▟████▙ ▜████████████████▛
+ ▟██████▙ ▜███▙
+ ▟███▛▜███▙ ▜███▙
+ ▟███▛ ▜███▙ ▜███▙
+ ▝▀▀▀ ▀▀▀▀▘ ▀▀▀▘
+```
+
+## References
+
+- https://elis.nu/blog/2019/08/encrypted-zfs-mirror-with-mirrored-boot-on-nixos/
+- https://blog.lazkani.io/posts/nixos-on-encrypted-zfs/
+- https://nixos.wiki/wiki/ZFS
diff --git a/src/content/posts/2022-07-24-mastery-based-learning.md b/src/content/posts/2022-07-24-mastery-based-learning.md
new file mode 100644
index 0000000..c25f827
--- /dev/null
+++ b/src/content/posts/2022-07-24-mastery-based-learning.md
@@ -0,0 +1,93 @@
+---
+title: "Mastery-Based Learning"
+date: 2022-07-24
+tags: ["education"]
+---
+
+A thought I've been brewing probably since undergrad is the idea of
+mastery-based education for skill-based practices. Directly inspired by the
+language learning apps, I wonder whether we can enhance a traditional spaced
+repetition system with a topic graph, where mastery can "spill" throughout the
+graph to better model learning. Since I'm never going to have time to actually
+build such a system, I thought I'd just jot these ideas down.
+
+### Knowledge Graph
+
+The first piece of this setup would require having an extensive knowledge graph.
+Think Wikipedia, where it has a lot of related topics, but rather than just
+being linked in an ad-hoc manner, each link has one or more of the following
+specific purposes:
+
+- **Dependency.** The linked topic needs some percentage of mastery in order
+ to best experience the current topic.
+
+- **Spill.** Not really sure what a good term for this would be, but basically
+ mastery of the current topic would result in some percentage of "spilled"
+ mastery gain for the linked topic.
+
+The dependency aspect allows people to work backwards, starting from what they
+don't know and being able to query what the required context is. They can build
+themselves a learning plan based on a topological sorting of those topics and
+tackle them individually.
+
+The spill aspect allows people to "skip" learning things they already know, for
+a faster onboarding experience. For example, since "the quadratic formula"
+requires someone to know "algebra", then if someone masters the quadratic
+formula before algebra, it should boost the mastery of algebra too.
+
+### Mastery Level
+
+I think the current way tests are handled are not only stressful, but a horrible
+way to measure mastery. Rather than promoting long-term learning, it encourages
+the cram-and-forget workflow. I think what the language learning apps taught us
+is not only is it good to repeat things when we get it wrong, it's also good to
+repeat things when we get it right.
+
+The vision would be something like this:
+
+1. First, the student learns some material. They take a short quiz immediately,
+ and their mastery is boosted by a small percentage depending on their score,
+ maybe up to 30%.
+
+2. Then, the student goes off and learns some related material. After a length
+ of time has passed, they are quizzed on the first topic again. By this time,
+ their mastery score should fall a bit simply on the basis of "forgetfulness
+ over time".
+
+3. At the end of the semester, if they have reached required thresholds of
+ mastery in each required topic, they will pass the class.
+
+Not only does this simplify final grading, it also removes the whole concept of
+stress in the middle, since doing badly on one exam doesn't hurt your grade
+permanently. On top of that, doing _well_ on a single exam doesn't guarantee
+that you know it, and the system models that by not giving you full mastery
+after a single test.
+
+But this doesn't necessarily mean that the student must re-take tests on things
+they already know. The great thing about the whole "spill" system is that if
+they learn topic A first, then topic B that depends on topic A, then topic B can
+indirectly keep topic A's mastery afloat.
+
+### Implementation Challenges
+
+Implementation is the toughest part. There's a couple technical hurdles I would
+like to complete before attempting such a system, which are:
+
+- A bunch of interactive widgets for allowing users to play around with the
+ material directly. This is more applicable in math and science curriculums.
+
+- Quiz generation software. There's probably good off-the-shelf components
+ already, I haven't looked.
+
+Another problem is that I never want to think about dealing with cheating. If
+this idea were to be neatly packaged up and deployed into schools, you bet the
+first problem teachers are going to have is with cheating. While there are some
+stopgaps such as auto-generated quizzes and personalized curriculums, there's
+never a guaranteed solution. Instead, fostering a healthy learning attitude
+among students is the best way for these systems to be effective.
+
+My final disclaimer is that I'm not an educator. I've TA'd for a functional
+programming course in undergrad and helped many peers learn programming concepts
+from time to time. Watching people learn is a very interesting process, and
+while I don't have time to conduct studies on how this process works, there's
+general patterns I picked up on while following this train of thought.
diff --git a/src/content/posts/2022-08-01-uiuctf-2022-writeups/easy-math.c b/src/content/posts/2022-08-01-uiuctf-2022-writeups/easy-math.c
new file mode 100644
index 0000000..5249564
--- /dev/null
+++ b/src/content/posts/2022-08-01-uiuctf-2022-writeups/easy-math.c
@@ -0,0 +1,60 @@
+#include
+#include
+#include
+#include
+#include
+
+#define MATH_PROBLEMS 10000
+
+int take_test() {
+ int urand = open("/dev/urandom", O_RDONLY);
+ if (!urand) return 1;
+ unsigned char urand_byte;
+
+ for (int i=0; i> 4;
+ printf("Question %d: %d * %d = ", i+1, a, b);
+
+ int ans;
+ if (scanf("%d", &ans) != 1) return 1;
+ if (ans != a * b) return 1;
+ }
+
+ close(urand);
+ return 0;
+}
+
+int check_id() {
+ printf("Checking your student ID...\n\n");
+ sleep(1);
+ struct stat real, given;
+ if (stat("/proc/1/fd/0", &real)) return 1;
+ if (fstat(0, &given)) return 1;
+ if (real.st_dev != given.st_dev) return 1;
+ if (real.st_ino != given.st_ino) return 1;
+ return 0;
+}
+
+int main() {
+ setreuid(geteuid(), getuid());
+ setvbuf(stdout, NULL, _IONBF, 0);
+
+ printf("Welcome to the MATH 101 final exam.\n");
+ if (check_id()) {
+ printf("The proctor kicks you out for pretending to be a student.\n");
+ return 1;
+ }
+
+ printf("The test begins now. You have three hours.\n\n");
+ alarm(3 * 60 * 60);
+ if (take_test()) {
+ printf("You have failed the test.\n");
+ return 1;
+ }
+
+ setreuid(getuid(), getuid());
+ system("cat /home/ctf/flag");
+ return 0;
+}
diff --git a/src/content/posts/2022-08-01-uiuctf-2022-writeups/frame.tar.gz b/src/content/posts/2022-08-01-uiuctf-2022-writeups/frame.tar.gz
new file mode 100644
index 0000000..d492f99
Binary files /dev/null and b/src/content/posts/2022-08-01-uiuctf-2022-writeups/frame.tar.gz differ
diff --git a/src/content/posts/2022-08-01-uiuctf-2022-writeups/index.md b/src/content/posts/2022-08-01-uiuctf-2022-writeups/index.md
new file mode 100644
index 0000000..636555d
--- /dev/null
+++ b/src/content/posts/2022-08-01-uiuctf-2022-writeups/index.md
@@ -0,0 +1,203 @@
+---
+title: "UIUCTF 2022 Writeups"
+date: 2022-08-01
+tags: ["ctf"]
+math: true
+---
+
+Last weekend I took some time on Friday to do UIUCTF 2022. I placed 102nd with
+462 points. Here are the writeups to the challenges I solved. My full workspace
+including partial work on unsolved challenges is published at
+[~mzhang/uiuctf-2022].
+
+[~mzhang/uiuctf-2022]: https://git.sr.ht/~mzhang/uiuctf-2022
+
+Thanks to @sampai, @vekt0r, and @# from the MIT osu! server for helping out
+with some of the challenges :)
+
+
+
+## Web: Frame - 50 points
+
+> "ornate wooden empty picture frame, on a teal wall"
+>
+> We made it easy to add a frame to your digital art! https://frame-web.chal.uiuc.tf/
+>
+> [handout.tar.gz](frame.tar.gz)
+
+This challenge prompted us to upload an image, and then it would display the
+image inside of a frame. Notably, this frame was done client-side, which means
+the original image was not post-processed in any way. If we look at the code
+that checks to make sure you uploaded a valid image:
+
+```php
+$allowed_extensions = array(".jpg", ".jpeg", ".png", ".gif");
+$filename = $_FILES["fileToUpload"]["name"];
+$tmpname = $_FILES["fileToUpload"]["tmp_name"];
+$target_file = "uploads/" . bin2hex(random_bytes(8)) . "-" .basename($filename);
+
+$has_extension = false;
+foreach ($allowed_extensions as $extension) {
+ if (strpos(strtolower($filename), $extension) !== false) {
+ $has_extension = true;
+ }
+}
+```
+
+The flaw here is that the file extension is only checked for existence, not that
+it actually occurs at the end of the file. As a result, the web server will
+guess the kind of data in the file based on the final extension. We can simply
+upload a file named `hello.jpg.php` and it will pass this.
+
+The Dockerfile in the handout helpfully tells us the location of the flag, so
+here is the file I uploaded:
+
+```
+cp real_image.jpg hello.jpg.php
+echo '' >> hello.jpg.php
+```
+
+Uploading this file reveals the flag.
+
+## Web: AR Pwny - 50 points
+
+> "a green cybernetic horse grazing in the sun"
+>
+> Welcome to the meataverse! http://ar-pwny-web.chal.uiuc.tf/
+>
+> [pwny.glb](pwny.glb)
+
+A glb file is a glTK texture. We can open this in a program such as [Blender] in
+order to understand it. Use **File > Import > glb** to open the file, then hide
+all of the objects except the two flag halves.
+
+[blender]: https://www.blender.org
+
+
+
+This reveals two QR codes that can be combined into the flag.
+
+## Pwn: easy math 1 - 88 points
+
+> Take a break from exploiting binaries, and solve a few\* simple math problems!
+>
+> `$ ssh ctf@easy-math.chal.uiuc.tf` password is `ctf`
+>
+> [easy-math.c](easy-math.c)
+
+This is really just a simple programming exercise. Looking at the source code,
+the annoying part is that it checks that your standard input is the same as the
+standard input of proc 1.
+
+This isn't too bad to get around, since we can just puppet the pseudoterminal of
+the SSH connection entirely using something like Paramiko:
+
+```python
+ssh = paramiko.SSHClient()
+ssh.set_missing_host_key_policy(paramiko.AutoAddPolicy())
+ssh.connect("easy-math.chal.uiuc.tf", 22, "ctf", "ctf")
+
+ch = ssh.invoke_shell()
+print(ch.recv(1024))
+```
+
+Looks like there was a more sneaky way of solving this challenge, which is what
+easy-math-2 went into, but I didn't spend enough time looking at this in order
+to figure it out.
+
+[solve script](https://git.sr.ht/~mzhang/uiuctf-2022/tree/master/item/pwn/easy-math-1/solve.py)
+
+## Crypto: Military Grade Encryption - 50 points
+
+> I came across a new website that claims to keep my flag safe with
+> military-grade encryption. Clearly, this is going to keep my flag safe from
+> anyone who may want it. https://military-grade-encryption-web.chal.uiuc.tf/
+
+I'm not really sure what the clever way to solve this was, but all the numbers
+were small enough to be brute forced, so that's what I did. Simply reverse the
+process used and look for a string beginning with `uiuctf{`.
+
+[solve script](https://git.sr.ht/~mzhang/uiuctf-2022/tree/master/item/crypto/military-grade-encryption/solve.py)
+
+## Crypto: asr - 85 points
+
+> Oh no I dropped my d. Good thing I'm not telling you my n.
+
+As this challenge implies, the problem comes from reversing the typical
+challenge of RSA. This time, rather than starting with a modulus and trying to
+discover the private exponent, we are given the private exponent, and trying to
+find the modulus.
+
+As a reminder, once we find $N$, we can simply evaluate $c^d \mod N$ to
+determine the final message.
+
+First, we know that the relationship between $e$ and $d$ is that $ed \equiv 1
+\mod \phi(N)$. Translating this to plain algebra, this means $ed - 1 = k\phi(N)$
+for some positive integer $k$. This tells us that $ed - 1$ must divide
+$\phi(N)$.
+
+We used an [external factoring service] to factor $ed - 1$. Using the
+`gen_prime` method given to us, we are able to validate that our factorization
+ended up being what was expected: exactly 16 64-bit primes, and a handful of
+smaller primes. The only thing left is organizing the 16 primes into two groups
+of 8.
+
+[external factoring service]: https://www.alpertron.com.ar/ECM.HTM
+
+Trusty old combinatorics tells us ${16 \choose 8} = 12870$, which is easily
+iterable within a matter of seconds. After picking 8 primes, we simply run
+through the same process as `gen_prime` in order to generate our $p$ and $q$:
+
+```python
+for perm in tqdm(perms):
+ perm = set(list(perm))
+ p = prod(perm)
+ q = prod(bigprimes - perm)
+
+ for i in range(7):
+ if isPrime(p + 1): break
+ p *= small_primes[i]
+ for i in range(7):
+ if isPrime(q + 1): break
+ q *= small_primes[i]
+
+ p = p + 1
+ q = q + 1
+```
+
+All that's left is to run $c^d \mod N$ and find strings that begin with
+`uiuctf{` to determine which of these organizations of prime factors is the
+correct one.
+
+[solve script](https://git.sr.ht/~mzhang/uiuctf-2022/tree/master/item/crypto/asr/solve2.py)
+
+## Wringing Rings - 139 points
+
+> Everyone says we should use finite fields, but I loved sharing secrets this
+> way so much that I put a ring on it!
+>
+> `$ nc ring.chal.uiuc.tf 1337`
+
+This challenge employs a variation of [Shamir's Secret Sharing algorithm][SSS].
+The crux of the algorithm involves encoding a shared secret into the
+coefficients of a polynomial of degree $k$. Note that given $k + 1$ unique
+points on this polynomial, the entire polynomial can be recovered. If $k$ is 6,
+and we generate 12 unique points to split between 12 people, then any individual
+must find 6 others in order to recover the secret.
+
+[SSS]: https://en.wikipedia.org/wiki/Shamir%27s_Secret_Sharing
+
+The problem with the implementation in question is that it does not operate over
+a finite field, as required by the original algorithm. This leaks information
+about the secret, specifically with respect to what numbers it divides, since we
+know that all coefficients must be integers.
+
+This means that even with the absence of one of the required points, we can
+still reasonably recover the curve with the added information that all
+coefficients are less than $500,000$.
+
+I simply threw all of the constraints we are given into the z3 solver, and
+within milliseconds the answer was given. After that it was just a matter of
+hooking it up to the challenge server and waiting for the flag.
+
+[solve script](https://git.sr.ht/~mzhang/uiuctf-2022/tree/master/item/crypto/wringing-rings/solve.py)
diff --git a/src/content/posts/2022-08-01-uiuctf-2022-writeups/pwny.glb b/src/content/posts/2022-08-01-uiuctf-2022-writeups/pwny.glb
new file mode 100644
index 0000000..5c385ea
Binary files /dev/null and b/src/content/posts/2022-08-01-uiuctf-2022-writeups/pwny.glb differ
diff --git a/src/content/posts/2022-09-20-higher-inductive-types.lagda.md b/src/content/posts/2022-09-20-higher-inductive-types.lagda.md
new file mode 100644
index 0000000..bdaf67b
--- /dev/null
+++ b/src/content/posts/2022-09-20-higher-inductive-types.lagda.md
@@ -0,0 +1,186 @@
+---
+title: "Higher Inductive Types"
+date: 2022-09-20
+tags: ["type-theory"]
+toc: true
+math: true
+draft: true
+---
+
+**Higher inductive types (HIT)** are central to developing cubical type theory.
+What this article will try to do is develop an approach to understanding higher
+inductive types based on my struggles to learn the topic.
+
+
+
+## Ordinary inductive types
+
+So first off, what is an inductive type? These are a kind of data structure
+that's commonly used in _functional programming_. For example, consider the
+definition of natural numbers (`Nat`):
+
+```agda
+data Nat : Set where
+ zero : Nat
+ suc : Nat → Nat
+```
+
+This defines all `Nat`s as either zero, or one more than another `Nat`. For
+example, here's the first few natural numbers and their corresponding
+representation using this data structure:
+
+```txt
+0 zero
+1 suc zero
+2 suc (suc zero)
+3 suc (suc (suc zero))
+4 suc (suc (suc (suc zero)))
+5 suc (suc (suc (suc (suc zero))))
+```
+
+Why is this representation useful? Well, if you remember **proof by induction**
+from maybe high school geometry, you'll recall that we can prove things about
+all natural numbers by simply proving that it's true for the _base case_ 0, and
+then proving that it's true for any _inductive case_ $n$, given that the
+previous case $n - 1$ is true.
+
+This kind of definition of natural numbers makes this induction structure much
+more clear. For example, look at the definition of a tree:
+
+```agda
+data Tree (A : Set) : Set where
+ leaf : A → Tree A
+ left : Tree A → Tree A
+ right : Tree A → Tree A
+```
+
+We can do induction on trees by simply proving it's true for (1) the base case,
+(2) the left case, and (3) the right case. In fact, all inductive data
+structures have this kind of induction principle. So say you wanted to prove
+that $1 + 2 + 3 + \cdots + n = \frac{n\cdot(n+1)}{2}$ for all $n \in
+\mathbb{N}$, then you could say:
+
+
+(click here for boring requisites)
+
+```agda
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; module ≡-Reasoning)
+open ≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; step-≡; _∎)
+open import Data.Product using (_×_)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Nat.DivMod using (_/_; 0/n≡0; n/n≡1; m*n/n≡m)
+open import Data.Nat.Properties using (+-assoc; *-identityˡ; *-comm; *-distribʳ-+; +-comm)
+
+sum-to-n : ℕ → ℕ
+sum-to-n zero = zero
+sum-to-n (suc x) = (suc x) + (sum-to-n x)
+
+distrib-/ : ∀ (a b c : ℕ) → a / c + b / c ≡ (a + b) / c
+distrib-/ zero b c =
+ begin
+ zero / c + b / c
+ ≡⟨ cong (_+ b / c) (0/n≡0 c) ⟩
+ b / c
+ ≡⟨ cong (_/ c) refl ⟩
+ (zero + b) / c
+ ∎
+distrib-/ (suc a) b c =
+ begin
+ (1 + a) / c + b / c
+ ≡⟨ cong (_+ b / c) (sym (distrib-/ 1 a c)) ⟩
+ 1 / c + a / c + b / c
+ ≡⟨ +-assoc (1 / c) (a / c) (b / c) ⟩
+ 1 / c + (a / c + b / c)
+ ≡⟨ cong (1 / c +_) (distrib-/ a b c) ⟩
+ 1 / c + (a + b) / c
+ ≡⟨ distrib-/ 1 (a + b) c ⟩
+ (suc a + b) / c
+ ∎
+```
+
+
+
+```agda
+-- Here's the proposition we want to prove:
+our-prop : ∀ (n : ℕ) → sum-to-n n ≡ n * (n + 1) / 2
+
+-- How do we prove this?
+-- Well, we know it's true for zero:
+base-case : sum-to-n 0 ≡ 0 * (0 + 1) / 2
+base-case = refl
+
+-- The next part is proving that it's true for any n + 1, given that it's true
+-- for the previous case n:
+inductive-case : ∀ {n : ℕ}
+ → (inductive-hypothesis : sum-to-n n ≡ n * (n + 1) / 2)
+ → sum-to-n (suc n) ≡ (suc n) * (suc n + 1) / 2
+```
+
+
+Inductive case proof, expand if you're interested
+
+```agda
+inductive-case {n} p =
+ begin
+ sum-to-n (suc n)
+ ≡⟨⟩ -- Expanding definition of sum-to-n
+ suc n + sum-to-n n
+ ≡⟨ cong (suc n +_) p ⟩ -- Substituting the previous case
+ suc n + n * (n + 1) / 2
+ ≡⟨ cong (_+ n * (n + 1) / 2) (sym (m*n/n≡m (suc n) 2)) ⟩
+ (suc n * 2) / 2 + (n * (n + 1)) / 2
+ ≡⟨ distrib-/ (suc n * 2) (n * (n + 1)) 2 ⟩
+ (suc n * 2 + n * (n + 1)) / 2
+ ≡⟨ cong (_/ 2) (cong (_+ n * (n + 1)) (*-comm (suc n) 2)) ⟩
+ (2 * suc n + n * (n + 1)) / 2
+ ≡⟨ cong (_/ 2) (cong (2 * suc n +_) (cong (n *_) (+-comm n 1))) ⟩
+ (2 * suc n + n * suc n) / 2
+ ≡⟨ cong (_/ 2) (sym (*-distribʳ-+ (suc n) 2 n)) ⟩
+ (1 + suc n) * suc n / 2
+ ≡⟨ cong (_/ 2) (cong (_* suc n) (+-comm 1 (suc n))) ⟩
+ (suc n + 1) * suc n / 2
+ ≡⟨ cong (_/ 2) (*-comm (suc n + 1) (suc n)) ⟩
+ (suc n) * (suc n + 1) / 2
+ ∎
+```
+
+
+
+So now that we have both the base and inductive cases, let's combine it using
+this:
+
+```agda
+-- Given any natural number property (p : ℕ → Set), if...
+any-nat-prop : (p : ℕ → Set)
+ -- ...it's true for the base case and...
+ → p 0
+ -- ...it's true for the inductive case...
+ → (∀ {n : ℕ} (a : p n) → p (suc n))
+ -- ...then the property is true for all naturals.
+ → (∀ (n : ℕ) → p n)
+any-nat-prop p base _ zero = base
+any-nat-prop p base ind (suc n) = ind (any-nat-prop p base ind n)
+```
+
+Then:
+
+```
+our-prop = any-nat-prop
+ (λ n → sum-to-n n ≡ n * (n + 1) / 2)
+ base-case inductive-case
+```
+
+Using Agda, we can see that this type-checks correctly.
+
+**TODO:** Ensure totality
+
+## Higher inductive types
+
+Moving on, we want to know what _higher_ inductive types brings to the table. To
+illustrate its effect, let's consider the following scenario: suppose you have
+
+#### References
+
+- [nLab](https://ncatlab.org/nlab/show/higher+inductive+type)
+- Section 2.5 of [Favonia's thesis](https://favonia.org/files/thesis.pdf)
+- [Quotient Types for Programmers](https://www.hedonisticlearning.com/posts/quotient-types-for-programmers.html)
diff --git a/src/content/posts/2022-10-27-dependent-types.md b/src/content/posts/2022-10-27-dependent-types.md
new file mode 100644
index 0000000..6353ff3
--- /dev/null
+++ b/src/content/posts/2022-10-27-dependent-types.md
@@ -0,0 +1,54 @@
+---
+title: "Dependent Types from First Principles"
+slug: "dependent-types"
+date: 2022-10-27
+tags: ["type-theory"]
+toc: true
+math: true
+draft: true
+---
+
+It's frequently said that computers are just made of 1s and 0s. As programmers,
+we induce structure into this sea of 1s and 0s to build a rich collection of
+abstractions that can produce the entire software ecosystem as we know it. But
+how does this work? Let's start from the beginning.
+
+### Bits and Bytes
+
+On the lowest level, your computer is actually a tiny network of many
+components, but let's pretend for a second it's just a giant list of **bits**.
+Something like this.
+
+```
+011101110110100001111001001000000110010001101001011001000010000001111001011011110111010100100000011001000110010101100011011011110110010001100101001000000111010001101000011010010111001100100000011011000110111101101100
+```
+
+This is often a mess, so we like to chunk these into groups of 8, called an
+_octet_, and then represent it as a 2-digit base 16 number. For example, the
+string above would look something like this:
+
+```
+77 68 79 20 64 69 64 20 79 6f 75 20 64 65 63 6f 64 65 20 74 68 69 73 20 6c 6f 6c
+```
+
+We've just turned our series of 1s and 0s into some numbers and letters. Great.
+Now what? How do we get programs, images, and video from this? Well, we have to
+induce some structure.
+
+### Building Blocks
+
+Suppose you had a pile of sugar and a pile of salt. They both look pretty
+similar, but if you were to put them into the same pile, cooking would be a
+disaster. You would not want to use salt where you wanted to use sugar, or vice
+versa.
+
+Same thing in computing. We have developed byte-level representations for
+several basic kinds of data, but without distinction, it's hard to tell them
+apart. So programmers developed **types**, ways of categorizing data so when
+we're just reading a series of 0s and 1s, we would know how to interpret it.
+
+| Raw | Interpreted as number | Interpreted as text |
+| ---------------- | --------------------- | ------------------- |
+| `68 65 6c 6c 6f` | 448,378,203,247 | `hello` |
+
+So now we know how to
diff --git a/src/content/posts/2022-10-30-decentralized-identity-middle-ground.md b/src/content/posts/2022-10-30-decentralized-identity-middle-ground.md
new file mode 100644
index 0000000..5c98cf9
--- /dev/null
+++ b/src/content/posts/2022-10-30-decentralized-identity-middle-ground.md
@@ -0,0 +1,65 @@
+---
+title: "Decentralized Identity, a Middle Ground"
+date: 2022-10-30T03:04:51-05:00
+logseq: true
+tags:
+ - web
+---
+
+- With Twitter management changing, I'm starting to think about the small web again. The small web is a concept where you use the Internet to interact with people directly, rather than operating through the medium of megacorps. When we think about big monoliths like Twitter and Facebook, at the very heart of it is some kind of algorithm picking what it is we see. And with the power to control that gives us advertising and mass manipulation.
+- For the rest of this blog post, I'll be talking about _microblogging_ specifically: short posts of several sentences, along with a few media attachments, of which Twitter is one of the largest monolithic implementations. But the things I talk about are also applicable to other applications, including long-form blogging (Medium), image sharing (Instagram, Snapchat), video sharing (YouTube), chat (Messenger)
+- There's several projects out there that are already trying out other extremes. I'll cover two big types here:
+ - **Federation.** This style of application development is inspired by email. The idea is that you develop a common _protocol_ for apps living on different servers to talk to each other, so you can have people choose their own servers rather than trusting everything to megacorps like Google or Facebook. One notable example of this in the microblogging realm is Mastodon / ActivityPub.
+ - **Peer-to-peer.** This style of application development is rarer, but can be seen commonly in things like torrents. The idea is that _each_ client holds all application info, and interacts with everything else as if they were all clients. One notable example of this in the microblogging realm is Scuttlebutt.
+- I'll go into more detail about these two styles later, but they both come with their advantages and drawbacks. However, I don't think any of the solutions that exist are sustainable for longer periods of time.
+- ## Feature Evaluation
+- One thing I've been doing recently when I think about software applications and system design is break things down into their **features**. This makes it a lot easier to compare applications or services to each other than a vague statement like "I've had a good/bad experience with this". So let's come up with some features of a good microblogging platform:
+ - Application design
+ - **Verifiability:** It should be easy to verify if I did indeed ever say something.
+ - **Freedom:** Within reason, I should not be limited in what I say or do on the platform.
+ - **Universality:** I should be able to communicate to anyone from anywhere (any device, any location).
+ - System design
+ - **Availability:** I want to be confident that the system will be around for many years.
+ - **Connectability:** I should be able to connect with people I don't already know easily.
+ - **Moderation:** I should be able to choose to not interact with a certain subset of users, and this process should not be painful.
+ - Scaling
+ - **User scaling:** Supporting more users should incur a relatively linear or sublinear cost, and should certainly not lead to resource consumption blowup.
+ - **Temporal scaling:** The system should support being run for an arbitrarily long amount of time.
+ - Development
+ - **Malleability:** How easy is it to introduce / roll out new versions and features? This may be important for updating cryptographic algorithms.
+ - **Version drift:** Is it possible to support users who are on different version of the service?
+- Some features are certainly more important than others, and may have different importance to different people. But it gives me a base line to evaluate services, and lets me decide which features I consider to be critical.
+- These are obviously not the only features, but I like to list them in this form because while some
+ alternative apps may tout certain features, it's useless if it falls short on something more important.
+- ### Evaluation
+- Now that we know what we're looking for, let's evaluate some existing services.
+- **Mastodon**
+ - Satisfies:
+ - **Connectability:** It's easy to find other users based on their user ID, which looks like an email so it's easy to share.
+ - Doesn't satisfy:
+ - **Freedom:** While certain instances may be specialized (i.e hobby-focused), it's certainly not great when you are locked out of communicating with someone on another instance because the admins of your respective instances have beef with each other.
+ - **Availability:** For some reason or another, I've seen Mastodon admins give up on their instances. Running an instance is very costly in terms of money and time, so it's not surprising that if an instance owner decides it's simply no longer worth it, the users are simply hosed. While there are some options for migration like redirection, it's useless if the original server doesn't stay online.
+- **Scuttlebutt**
+ - Satisfies:
+ - **Freedom:** This is the maximally free solution: your client is solely responsible for receiving and filtering all messages.
+ - Doesn't satisfy:
+ - **Connectability:** Connecting with someone must take place over an existing channel (i.e either meeting in meatspace or sharing a pub). If I don't have my Scuttlebutt client with me, then it's not possible to get updates.
+ - **Universality:** Since user identity is heavily tied to a single client, having multiple clients for a single user is not a well-supported workflow.
+- The Matrix people have also developed [Cerulean], a playground for testing the idea of _relative reputation_, where instead of doing moderation of all users you can assign a web-of-trust-style reputation to people you follow. However, this may lead to further filter-bubbling, the implications of which I'm honestly not sure how to tackle.
+
+ [Cerulean]: https://matrix.org/blog/2020/12/18/introducing-cerulean#whats-with-the-decentralised-reputation-button
+
+- ## Decentralized Identity
+- My view for an ideal microblogging platform would be a federated server-client architecture, but where a user identity isn't tied to the server the same way a user is tied to their Mastodon instance. Essentially, you want your account to be promiscuous between several servers.
+- This way, you gain all of the benefits of having a server-client architecture (easy to do multiple clients), while not relying on the server itself or its admins to stay around for a long time.
+- The problem is, designing such a system securely is difficult. Ultimately, what I'm proposing is:
+ - A user identity model based on an asymmetric-key model. Users generate their own key locally and provide it to instances.
+ - Users should then have _client_ keys, which are independent of the user keys. These are signed by the user key to indicate that they belong to the same user.
+ - When a user wants to switch servers, they can begin requesting a checkout of their data from the server. The data can be signed by the server as well to provide an indicator that the client isn't trying to forge old history.
+ - One problem is if a server wants to deny a user from switching servers; they may try to keep the data hostage. One solution is just to scrape all publicly obtainable data, the other is to hope that this is socially discouraged by just having users avoid servers that engage in user-hostile actions.
+ - Users may also opt to replicate their identity entirely between two servers. This just means that this synchronization process is just happening incrementally or periodically rather than just at switch-time.
+- This still has a number of open problems:
+ - **Key revocation.** Obviously, anything involving cryptographic keys requires a revocation protocol in the event that the keys are compromised. I'm not too sure of a good way of doing this that doesn't involve an infinitely growing append-only list of revocations on all of the people who have
+- When I have some free time, I may take a crack at a proof-of-concept implementation of a system like this.
+- ### Further applications
+- Since this scheme only really targets the identity layer with (theoretically) asymptotically constant change required for other parts of the software, this should be able to be extended to things other than just microblogging. I'm not sure about the level of success this may have for things like sharing large data files such as video (maybe mix in something like IPFS?), but there is certainly room for exploration.
diff --git a/src/content/posts/2022-10-30-rust-impure-path.md b/src/content/posts/2022-10-30-rust-impure-path.md
new file mode 100644
index 0000000..0991190
--- /dev/null
+++ b/src/content/posts/2022-10-30-rust-impure-path.md
@@ -0,0 +1,38 @@
+---
+title: "Rust's Impure Path"
+date: 2022-10-30T12:47:41-05:00
+languages: ["rust"]
+tags: ["rust"]
+---
+
+I work on [garbage], a project that touches the filesystem a lot. Because of
+this, I'd really like to control when and where these filesystem accesses
+happen.
+
+[garbage]: https://git.sr.ht/~mzhang/garbage
+
+The Rust standard library has a `fs` module, which I expect to _exclusively_
+contain filesystem access primitives. But actually a lot of the functionality
+also gets leaked into `std::path::Path`.
+
+In my ideal world, `Path` only deals with the data in a path, not its
+interaction with the filesystem. So it should never be able to check whether or
+not a path [exists], for example, or if a path [is a symlink][is_symlink]. Those
+should be delegated to something within `fs`.
+
+[exists]: https://doc.rust-lang.org/stable/std/path/struct.Path.html#method.exists
+[is_symlink]: https://doc.rust-lang.org/stable/std/path/struct.Path.html#method.is_symlink
+
+In addition, many of these functions automatically resolve symlinks, without
+built-in ways of achieving the same functionality without resolving symlinks, so
+I ended up having to fill those in myself. For example, I really just expect
+[`canonicalize`] to be an in-memory manipulation of path components.
+
+[`canonicalize`]: https://doc.rust-lang.org/stable/std/path/struct.Path.html#method.canonicalize
+
+Honestly, I've got to give it to Python's [pathlib], which solves the problems I
+noted above. It splits the path API into `Path` and `PurePath`, the latter of
+which does not make any IO accesses. It also provides non-symlink-resolving and
+symlink-resolving variants of converting to absolute paths.
+
+[pathlib]: https://docs.python.org/3/library/pathlib.html
diff --git a/src/content/posts/2023-03-26-inductive-types.md b/src/content/posts/2023-03-26-inductive-types.md
new file mode 100644
index 0000000..856e8c3
--- /dev/null
+++ b/src/content/posts/2023-03-26-inductive-types.md
@@ -0,0 +1,308 @@
+---
+title: "Inductive Types"
+date: 2023-03-26
+tags: ["type-theory"]
+math: true
+draft: true
+toc: true
+language_switcher_languages: ["ocaml", "python"]
+---
+
+There's a feature common to many functional languages, the ability to have
+algebraic data types. It might look something like this:
+
+{{< language-switcher >}}
+
+```ocaml
+type bool =
+| True
+| False
+```
+
+For those who are unfamiliar with the syntax, I'm defining a type called `bool`
+that has two _constructors_, or ways to create this type. The constructors are
+`True` and `False`. This means:
+
+1. Any time I use the value `True`, it's understood to have type `bool`.
+2. Any time I use the value `False`, it's understood to have type `bool`.
+3. In addition, there are _no_ other ways to create values of `bool` other than combining `True` and `False` constructors.
+
+---
+
+```python
+from typing import Literal
+MyBool = Literal[True] | Literal[False]
+```
+
+{{}}
+
+> **Note:** I'm using an experimental language switcher. It's implemented in
+> pure CSS using a feature called the [`:has` pseudo-class][has]. As of writing,
+> all major browsers _except_ Firefox has it implemented and enabled by default.
+> For Firefox there does exist a feature flag in about:config, but your mileage
+> may vary.
+
+---
+
+Many languages have this feature, under different names. Tagged unions, variant
+types, enumerations, but they all reflect a basic idea: a type with a limited
+set of variants.
+
+Now, in type theory, one of the interesting things to know about a type is its
+_cardinality_. For example, the type `Boolean` is defined to have cardinality 2.
+That's because there's only one constructor, so if at any point you have some
+unknown value of type `Boolean`, you know it can only take one of two values.
+
+
+ Note about Booleans
+
+There's actually nothing special about boolean itself. I could just as easily
+define a new type, like this:
+
+{{< language-switcher >}}
+
+```ocaml
+type WeirdType =
+| Foo
+| Bar
+```
+
+---
+
+```python
+from typing import Literal
+WeirdType = Literal['foo'] | Literal['bar']
+```
+
+{{}}
+
+Because this type can only have two values, it's _semantically_ equivalent to
+the `Boolean` type. I could use it anywhere I would typically use `Boolean`.
+
+I would have to define my own operators such as AND and OR separately, but
+those aren't properties of the `Boolean` type itself, they are properties of
+the Boolean algebra, which has several [algebraic properties][1] such as
+associativity, commutativity, distributivity, and several others. Think of it
+as a sort of _interface_, where if you can implement that interface, your type
+qualifies as a Boolean algebra!
+
+[1]: https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Definition
+
+
+
+You can make any _finite_ type like this: just create an algebraic data type
+with unit constructors, and the result is a type with a finite cardinality. If I
+wanted to make a unit type for example:
+
+{{< language-switcher >}}
+
+```ocaml
+type unit =
+| Unit
+```
+
+---
+
+```python
+from typing import Literal
+Unit = Literal[None]
+```
+
+{{}}
+
+There's only one way to ever construct something of this type, so the
+cardinality of this type would be 1.
+
+## Doing things with types
+
+Creating types and making values of those data types is just the first part
+though. It would be completely uninteresting if all we could do is create types.
+So, the way we typically use these types is through _pattern matching_ (also
+called structural matching in some languages).
+
+Let's see an example. Suppose I have a type with three values, defined like
+this:
+
+{{< language-switcher >}}
+
+```ocaml
+type direction =
+| Left
+| Middle
+| Right
+```
+
+---
+
+```python
+from typing import Literal
+Direction = Literal['left'] | Literal['middle'] | Literal['right']
+```
+
+{{}}
+
+If I was given a value with a type of direction, but I wanted to do different
+things depending on exactly which direction it was, I could use _pattern
+matching_ like this:
+
+{{< language-switcher >}}
+
+```ocaml
+let do_something_with (d : direction) =
+ match d with
+ | Left -> do_this_if_left
+ | Middle -> do_this_if_middle
+ | Right -> do_this_if_right
+```
+
+---
+
+```python
+def do_something_with(d : Direction) -> str:
+ match inp:
+ case 'left': return do_this_if_left
+ case 'middle': return do_this_if_middle
+ case 'right': return do_this_if_right
+ case _: assert_never(inp)
+```
+
+**Note:** the `assert_never` is a static check for exhaustiveness. If we missed
+a single one of the cases, a static type checker like [pyright] could catch it
+and tell us which of the remaining cases there are.
+
+[pyright]: https://github.com/microsoft/pyright
+
+{{}}
+
+This gives me a way to discriminate between the different variants of
+`direction`.
+
+> Most languages have a built-in construct for discriminating between values of
+> the `Boolean` type, called if-else. What would if-else look like if you wrote
+> it as a function in this pattern-matching form?
+
+## Constructing larger types
+
+Finite-cardinality types like the ones we looked at just now are nice, but
+they're not super interesting. If you had a programming language with nothing
+but those, it would be very painful to write in! This is where _type
+constructors_ come in.
+
+When I say type constructor, I mean a type that can take types and build other
+types out of them. There's several ways this can be done, but the one I want to
+discuss today is called _inductive_ types.
+
+> If you don't know what induction is, the [Wikipedia article][2] on it is a
+> great place to start!
+>
+> [2]: https://en.wikipedia.org/wiki/Mathematical_induction
+
+The general idea is that we can build types using either base cases (variants
+that don't contain themselves as a type), or inductive cases (variants that _do_
+contain themselves as a type).
+
+You can see an example of this here:
+
+{{< language-switcher >}}
+
+```ocaml
+type nat =
+| Suc of nat
+| Zero
+```
+
+{{}}
+
+These are the natural numbers, which are defined inductively. Each number is
+just represented by a data type that wraps 0 that number of times. So 3 would be
+`Suc (Suc (Suc Zero))`.
+
+At this point you can probably see why these have _infinite_ cardinality: with
+the Suc case, you can keep wrapping nats as many times as you want!
+
+One key observation here is that although the _cardinality_ of the entire type is
+infinite, it only uses _two_ constructors to build it. This also means that if
+we want to talk about writing any functions on `nat`, we just have to supply 2
+cases instead of an infinite number of cases:
+
+```ocaml
+let rec is_even = fun (n : nat) ->
+ match n with
+ | Zero -> true
+ | Suc n1 -> not (is_even n1)
+```
+
+
+ Try it for yourself
+
+If you've got an OCaml interpreter handy, try a couple values for yourself and
+convince yourself that this accurately represents the naturals and an even
+testing function:
+
+```ocaml
+utop # is_even Zero;;
+- : bool = true
+utop # is_even (Suc Zero);;
+- : bool = false
+```
+
+This is a good way of making sure the functions you write make sense!
+
+
+
+## Induction principle
+
+Let's express this in the language of mathematical induction. If I have any
+natural number:
+
+- If the natural number is the base case of zero, then the `is_even` relation
+ automatically evaluates to true.
+- If the natural number is a successor, invert the induction hypothesis (which is
+ what `is_even` evaluates to for the previous step, a.k.a whether or not the
+ previous natural number is even), since every even number is succeeded by
+ an odd number and vice versa.
+
+Once these rules are followed, by induction we know that `is_even` can run on
+any natural number ever. In code, this looks like:
+
+```ocaml
+let is_even
+ (n_zero : bool)
+ (n_suc : nat -> bool)
+ (n : nat)
+ : bool =
+ match n with
+ | Zero -> n_zero
+ | Suc n1 -> n_suc n1
+```
+
+where n_zero defines what to do with the zero case, and n_suc defines what to do
+with the successor case.
+
+You might've noticed that this definition doesn't actually return any booleans.
+That's because this is not actually the is_even function! This is a general
+function that turns any natural into a boolean. In fact, we can go one step
+further and generalize this to all types:
+
+```ocaml
+let nat_transformer
+ (n_zero : 'a)
+ (n_suc : 'a -> 'a)
+ (n : nat)
+ : 'a =
+ match n with
+ | Zero -> n_zero
+ | Suc n1 -> n_suc n1
+```
+
+Let's say I wanted to write a function that converts from our custom-defined nat
+type into an OCaml integer. Using this constructor, that would look something
+like this:
+
+```ocaml
+let convert_nat = nat_transformer 0 (fun x -> x + 1)
+```
+
+TODO: Talk about https://counterexamples.org/currys-paradox.html
+
+[has]: https://developer.mozilla.org/en-US/docs/Web/CSS/:has
diff --git a/src/content/posts/2023-03-29-shell-in-docker-compose-container-without-shell.md b/src/content/posts/2023-03-29-shell-in-docker-compose-container-without-shell.md
new file mode 100644
index 0000000..dd672e6
--- /dev/null
+++ b/src/content/posts/2023-03-29-shell-in-docker-compose-container-without-shell.md
@@ -0,0 +1,83 @@
+---
+title: "Getting a shell in a Docker Compose container without any shells"
+date: 2023-03-29
+tags: ["docker", "linux"]
+---
+
+First (published) blog post of the year! :raising_hands:
+
+Here is a rather dumb way of entering a Docker Compose container that didn't
+have a shell. In this specific case, I was trying to enter a Woodpecker CI
+container without exiting it. Some Docker containers are incredibly stripped
+down to optimize away bloat (which is good!) but this may make debugging them
+relatively annoying.
+
+> These are my specific steps for running it, please replace the paths and
+> container names with the ones relevant to your specific use-case.
+
+At first, I tried an approach following [this][1] document. But once I got to
+actually running commands within the namespace, I realized that this exposes the
+exact same interface as Docker compose; if there was no shell available from the
+Docker container entirely, then I couldn't run something from outside. I would
+need to get some shell into the container.
+
+[1]: https://www.redhat.com/sysadmin/container-namespaces-nsenter
+
+Fortunately, there's a software that contains a lot of handy tools in one
+binary: [busybox][2]. It's a GPL software that contains a small implementation
+of some coreutils (the Unix utilities like `ls` and `cp`) in a single static
+binary.
+
+[2]: https://busybox.net/
+
+I grabbed a copy of the busybox tool using:
+
+```
+$ nix build nixpkgs#pkgsStatic.busybox
+```
+
+(if you aren't using [Nix][3], you may want to grab one of the pre-built
+binaries from their website)
+
+[3]: https://nixos.org/
+
+To make sure it's statically linked (this means it doesn't depend on any
+libraries already existing on your system, which may not be available within the
+container), run this:
+
+```
+$ ldd ./result/bin/busybox
+ not a dynamic executable
+```
+
+You should be all good if it comes back with "not a dynamic executable".
+Otherwise, if you're downloading off the website, make sure you look for
+something that indicates you're downloading a version built with [`musl`][4],
+which means it's using a static implementation of libc.
+
+[4]: https://musl.libc.org/
+
+Now it's just a matter of getting this binary into the container.
+
+```
+$ docker compose cp ./result/bin/busybox woodpecker-server:/
+```
+
+Now, I can run a shell, using the busybox program:
+
+```
+$ docker compose exec woodpecker-server /busybox sh
+/ #
+```
+
+If you just ran busybox without the `sh` param, then it would list all the
+busybox utilities that were built into your static binary. At this point, I also
+ran:
+
+```
+/ # /busybox --install -s /bin
+```
+
+within the container. This installs symlinks to busybox so it acts as each of
+the individual programs it emulates. Now I can type `ls` instead of having to
+run `busybox ls` every single time.
diff --git a/src/content/posts/2023-04-20-developing-without-flake.md b/src/content/posts/2023-04-20-developing-without-flake.md
new file mode 100644
index 0000000..a693607
--- /dev/null
+++ b/src/content/posts/2023-04-20-developing-without-flake.md
@@ -0,0 +1,154 @@
+---
+title: "Developing on projects without flake.nix on NixOS"
+date: 2023-04-20
+tags: ["linux", "nixos"]
+---
+
+Ever since I became a NixOS hobbyist a few years ago, it's easy to plug NixOS
+wherever I go. The way flakes create a reproducible development environment
+across projects is so easy. I could clone any repository with a `flake.nix` or a
+`shell.nix` file, run a simple `nix develop` (or `nix-shell`), and be completely
+ready to start writing code without doing any additional setup. It configures
+both the dependencies and environment variables I need and plops me straight
+into a shell that has everything set up.
+
+```
+michael in 🌐 molecule in liveterm on master [⇡] is 📦 v0.1.0 via 🦀 v1.68.0-nightly
+❯ nix develop
+
+[michael@molecule:~/Projects/liveterm]$ █
+```
+
+To make things even easier, [direnv] (along with [nix-direnv]) can insert shell
+hooks so that I don't even have to run any commands; just going into the
+directory itself triggers a hook that sets up my current shell, so I can keep
+all of my fancy prompts and highlighting and other shell features.
+
+```
+michael in 🌐 molecule in ~
+❯ j liveterm
+/home/michael/Projects/liveterm
+direnv: loading ~/Projects/liveterm/.envrc
+direnv: using flake
+direnv: nix-direnv: using cached dev shell
+direnv: using flake
+direnv: nix-direnv: using cached dev shell
+direnv: export +AR +AS +CC +CONFIG_SHELL +CXX +DETERMINISTIC_BUILD +HOST_PATH +IN_NIX_SHELL +LD +NIX_BINTOOLS +NIX_BINTOOLS_WRAPPER_TARGET_HOST_x86_64_unknown_linux_gnu +NIX_BUILD_CORES +NIX_CC +NIX_CC_WRAPPER_TARGET_HOST_x86_64_unknown_linux_gnu +NIX_CFLAGS_COMPILE +NIX_ENFORCE_NO_NATIVE +NIX_HARDENING_ENABLE +NIX_INDENT_MAKE +NIX_LDFLAGS +NIX_PKG_CONFIG_WRAPPER_TARGET_HOST_x86_64_unknown_linux_gnu +NIX_SSL_CERT_FILE +NIX_STORE +NM +OBJCOPY +OBJDUMP +PKG_CONFIG +PKG_CONFIG_PATH +PYTHONHASHSEED +PYTHONNOUSERSITE +PYTHONPATH +RANLIB +READELF +SIZE +SOURCE_DATE_EPOCH +STRINGS +STRIP +SYSTEM_CERTIFICATE_PATH +_PYTHON_HOST_PLATFORM +_PYTHON_SYSCONFIGDATA_NAME +buildInputs +buildPhase +builder +cmakeFlags +configureFlags +depsBuildBuild +depsBuildBuildPropagated +depsBuildTarget +depsBuildTargetPropagated +depsHostHost +depsHostHostPropagated +depsTargetTarget +depsTargetTargetPropagated +doCheck +doInstallCheck +dontAddDisableDepTrack +mesonFlags +name +nativeBuildInputs +out +outputs +patches +phases +propagatedBuildInputs +propagatedNativeBuildInputs +shell +shellHook +stdenv +strictDeps +system ~PATH ~XDG_DATA_DIRS
+
+michael in 🌐 molecule in liveterm on master [⇡] is 📦 v0.1.0 via 🦀 v1.68.0-nightly via ❄️ impure (nix-shell)
+❯ █
+```
+
+The reason behind this is that on NixOS, I am able to prevent cluttering my
+global environment with project-specific configurations. While I do still have a
+global Node and Python for testing one-off things, all of my projects have their
+own flake file, that locks specific versions of Node and Python so I can be sure
+it builds in the future.
+
+But what about projects that don't have a flake definition file? Without some
+kind of existing configuration, I have _no_ dependencies, and if I want to even
+build it, I would have to write a flake myself. That's fine and all, but
+typically the `flake.nix` file lives in the root directory of the project, and
+it's good practice in the Nix world to commit the flake file along with its
+corresponding lock file. However, the upstream project may not appreciate it if
+I shove new config files in their root directory.
+
+```
+ project
+ ...
+ .envrc ✗
+ flake.lock ✗
+ flake.nix ✗
+```
+
+> The `✗` indicates that I added the file to the project, and it hasn't been
+> committed to the repo yet.
+
+One way to fix this is just to never commit the flake file. Always use explicit
+names with `git add`, and constantly check `git status` to make sure the file
+isn't committed. While this is good practice anyway, it gets quite cumbersome.
+Some upstream projects may also be ok with adding entries into the `.gitignore`
+file for the flake files, but I wouldn't be writing about it if these were the
+only solutions!
+
+### Separating the flake from the repo
+
+[direnv] uses a file called `.envrc` to configure setup instructions whenever you
+go into the directory (or subdirectories). For a normal flake setup, a simple
+config would look something like this:
+
+```
+use flake
+```
+
+This would query for the default dev shell found in the current directory's
+flake and set up my current shell accordingly. I figured this would probably
+take parameters, and unsurprisingly, it does! So my approach is just to create a
+separate directory alongside the git repository that just contains Nix flake
+files.
+
+```
+ project
+ ...
+ .envrc ✗
+ project-dev-flake
+ flake.lock
+ flake.nix
+```
+
+Now, the flake exists in a separate directory outside of the git repo. Now
+`.envrc` needs to be updated to point to this new directory:
+
+```
+use flake /path/to/project-dev-flake
+```
+
+If you have multiple dev shells, you can also use the `project-dev-flake#shell`
+syntax to point to whichever shell you would like to automatically enter.
+
+---
+
+Ok great, now the flake file's out of the way. But we still have this `.envrc`
+that needs to exist. This file defines the behavior of the shell hook of the
+directory we're in, so in the repo for us for the hook to trigger ...right?
+
+### Separating the `.envrc` file from the repo
+
+So actually, the `.envrc` file conveniently affects all of the subdirectories of
+the directory the file is in, not just the current one. This way if you `cd`
+somewhere within your project hierarchy, you're not losing all the shell hook
+behavior.
+
+We can use this by moving the git repo _into_ the dev flake instead. So now the
+project structure should look a bit more like this:
+
+```
+ project-dev-flake
+ project
+ .envrc
+ flake.lock
+ flake.nix
+```
+
+> Remember, since you moved the `.envrc` file, you will need to run `direnv
+allow` again. Depending on how you moved it, you might also need to change the
+> path you wrote in the `use flake` command.
+
+With this setup, the `project` directory can contain a clean clone of upstream
+and your flake files will create the appropriate environment.
+
+This _does_ create an extra layer of directory nesting, but except for copying
+longer paths, it really doesn't hurt my workflow. I use [autojump], which
+automatically just remembers where paths are, so I can just type `j `
+to go to my project's directory directly. It's sorted by frequency, so as long
+as I don't visit the `-dev-flake` container directory more often, my workflow
+doesn't change at all.
+
+---
+
+I hope this helps you set up projects to contribute to non-NixOS projects a bit
+easier!
+
+[direnv]: https://direnv.net/
+[nix-direnv]: https://github.com/nix-community/nix-direnv
+[autojump]: https://github.com/wting/autojump
diff --git a/src/content/posts/2023-04-20-programmable-proofs.md b/src/content/posts/2023-04-20-programmable-proofs.md
new file mode 100644
index 0000000..1c71770
--- /dev/null
+++ b/src/content/posts/2023-04-20-programmable-proofs.md
@@ -0,0 +1,437 @@
+---
+title: "Programmable Proofs"
+date: 2023-04-20
+tags: ["type-theory"]
+math: true
+draft: true
+---
+
+Today I'm going to convince you that data types in programming are the same as
+[_propositions_][proposition] in the logical sense. Using this, we can build an
+entire proof system on top of a programming language and verify mathematical
+statements purely with programs.
+
+To make this idea more approachable, I'm going to stick to using [Typescript]
+for some of the starting examples to explain the concepts. Then, we'll go and
+see how this stacks up in a language designed for writing mathematical proofs.
+
+---
+
+If we're going to talk about type theory, let's start by bringing some types to
+the table. In Typescript, there's a very simple way to create a type: defining a
+class! We can make new classes in Typescript like this:
+
+```ts
+class Cake {}
+```
+
+Simple enough. `Cake` is a type now. What does being a type mean?
+
+- We can make some `Cake` like this:
+
+ ```ts
+ let cake1 = new Cake();
+ let cake2 = new Cake();
+ ```
+
+- We can use it in function definitions, like this:
+
+ ```ts
+ function giveMeCake(cake: Cake) {
+ /* ... */
+ }
+ ```
+
+- We can put it in other types, like this:
+
+ ```ts
+ type Party = { cake: Cake; balloons: Balloon[] /* ... */ };
+ ```
+
+ This creates a `Party` object that contains a `Cake`, some `Balloon`s, and
+ possibly some other things.
+
+Ok that's cool. But we're curious people, so suppose we decide to have some fun
+and make a class that doesn't have a constructor:
+
+```ts
+class NoCake {
+ private constructor() {}
+}
+```
+
+> I admit, there still is a constructor, but just a private one, which means you
+> can't call it from outside the class. Same thing in effect.
+
+In Typescript and many OO languages it's based on, classes are given public
+constructors by default. This lets anyone create an instance of the class, and
+get all the great benefits we just talked about above. But when we lock down the
+constructor, we can't just freely create instances of this class anymore.
+
+
+ Why might we want to have private constructors?
+
+Let's say you had integer user IDs, and in your application whenever you wrote
+a helper function that had to deal with user IDs, you had to first check that
+it was a valid ID:
+
+```ts
+/** @throws {Error} */
+function getUsername(id: number): string {
+ // First, check if id is even a valid id...
+ if (!isIdValid(id)) throw new Error("Invalid ID");
+
+ // Ok, now we are sure that id is valid.
+ // ...
+}
+```
+
+It would be really nice if we could make a type to encapsulate this, so that
+we know that every instance of this class was a valid id, rather than passing
+around numbers and doing the check every time.
+
+```ts
+function getUsername(id: UserId): string {
+ // We can just skip the first part entirely now!
+ // Because of the type of the input, we are sure that id is valid.
+ // ...
+}
+```
+
+Note that the function also won't throw an exception for an invalid id
+anymore! That's because we're moving the check somewhere else. You could
+probably imagine what an implementation of this "somewhere else" looks like:
+
+```ts
+class UserId {
+ private id: number;
+
+ /** @throws {Error} */
+ constructor(id: number) {
+ // First, check if id is even a valid id...
+ if (!isIdValid(id)) throw new Error("Invalid ID");
+
+ this.id = number;
+ }
+}
+```
+
+This is one way to do it. But throwing exceptions from constructors is
+typically bad practice. This is because constructors are meant to be the final
+step in creating a particular object and should always return successfully and
+not have side effects. So in reality, what we want is to put this into a
+_static method_ that can create `UserId` objects:
+
+```ts
+class UserId {
+ private id: number;
+ constructor(id: number) {
+ this.id = id;
+ }
+
+ /** @throws {Error} */
+ fromNumberChecked() {
+ // First, check if id is even a valid id...
+ if (!isIdValid(id)) throw new Error("Invalid ID");
+ return new UserId(id);
+ }
+}
+```
+
+But this doesn't work if the constructor is also public, because someone can
+just **bypass** this check function and call the constructor anyway with an
+invalid id! We need to limit the constructor, so that all attempts to create
+a `UserId` instance goes through our function:
+
+```ts
+class UserId {
+ private id: number;
+ private constructor(id: number) {
+ this.id = id;
+ }
+
+ /** @throws {Error} */
+ fromNumberChecked() {
+ // First, check if id is even a valid id...
+ if (!isIdValid(id)) throw new Error("Invalid ID");
+ return new UserId(id);
+ }
+}
+```
+
+Now we can rest assured that no matter what, if I get passed a `UserId`
+object, it's going to be valid.
+
+```ts
+function getUsername(id: UserId): string {
+ // We can just skip the first part entirely now!
+ // Because of the type of the input, we are sure that id is valid.
+ // ...
+}
+```
+
+This works for all kinds of validations, as long as the validation is
+_permanent_. So actually in our example, a user could get deleted while we
+still have `UserId` objects lying around, so the validity would not be true.
+But if we've checked that an email is of the correct form, for example, then
+we know it's valid forever.
+
+
+
+Let's keep going down this `NoCake` example, and suppose we never implemented
+any other static methods that would call this constructor either. That's the
+full implementation of this class. We have now guaranteed that _no one can ever
+create an instance of this class_.
+
+But what about our use cases?
+
+- We can no longer make `NoCake`. This produces a method visibility error:
+
+ ```ts
+ let cake = new NoCake();
+ ```
+
+ You'll get an error that reads something like this:
+
+ > Constructor of class `NoCake` is private and only accessible within the class declaration.
+
+- We can no longer use it in function definitions or type constructors, like
+ this:
+
+ ```ts
+ function giveMeCake(cake: NoCake) {
+ /* ... */
+ }
+ type Party = { cake: NoCake; balloons: Balloon[] /* ... */ };
+ ```
+
+ Interestingly, this actually still typechecks! Why is that?
+
+ The reason is that even though you can never actually call this function, the
+ _definition_ of the function is still valid. (the more technical reason behind
+ this has to do with the positivity of variables, but that's a discussion for a
+ later day)
+
+ In fact, functions and types like this will actually be very useful for us
+ later on. Think about what happens to `Party` if one of its required elements
+ is something that can never be created.
+
+ No cake, no party! The `Party` type _also_ can't ever be constructed. The
+ _type_ called `Party` still exists, we just can't produce an object that will
+ qualify as a `Party`.
+
+We've actually created a very important concept in type theory, known as the
+**bottom type**. In math, this corresponds to $\emptyset$, or the _empty set_,
+but in logic and type theory we typically write it as $\bot$ and read it as
+"bottom".
+
+What this represents is a concept of impossibility. If a function requires an
+instance of a bottom type, it can never be called, and if a type constructor
+requires a bottom type, like `Party`, it can never be constructed.
+
+Typescript actually has the concept of the bottom type baked into the language:
+[`never`][never]. So we never actually needed to create this `NoCake` type at
+all! We could've just used `never`. It's used to describe computations that
+never produce a value. For example, consider the following functions:
+
+```ts
+// Throw an error
+function never1(): never {
+ throw new Error("fail");
+}
+
+// Infinite loop
+function never2(): never {
+ while (true) {
+ /* no breaks */
+ }
+}
+```
+
+The reason why these are both considered `never`, or $\bot$-types, is because
+imagine using this in a program:
+
+```ts
+function usingNever() {
+ let canThisValueExist = never1();
+ console.log(canThisValueExist);
+}
+```
+
+You can _never_ assign a value to the variable `canThisValueExist`, because the
+program will never reach the log statement, or any of the statements after it.
+The `throw` will bubble up and throw up before you get a chance to use the value
+after it, and the infinite loop will never even finish, so nothing after it will
+ever get run.
+
+We can actually confirm that the `never` type can represent logical falsehood,
+by using one of the "features" of false, which is that ["false implies
+anything"][false]. In code, this looks like:
+
+```ts
+function exFalso(x: never): T {
+ return x;
+}
+```
+
+You'll notice that even though this function returns `T`, you can just return
+`x` and the typechecker is satisfied with it. Typescript bakes this behavior
+into the subtyping rules of `never`, so `never` type-checks as any other type,
+so for example you can't do this easily with our `NoCake` type.
+
+```ts
+// Does not type-check!
+function notExFalso(x: NoCake): T {
+ return x;
+}
+```
+
+Ok, we've covered bottom types, and established that it's analogous to logical
+falsehood. But what represents logical truth?
+
+Well, here's where we have to talk about what truth means. There's two big
+parties of logical thought that are involved here. Let's meet them:
+
+- **Classical logic**: gets its name from distinguishing itself from
+ intuitionistic logic. In this logical system, we can make statements and
+ talk about their truth value. As long as we've created a series of logical
+ arguments from the axioms at the start to get to "true", we're all good.
+ Under this framework, we can talk about things without knowing what they
+ are, so we can prove things like "given many non-empty sets, we can choose one
+ item out of each set" without actually being able to name any items or a way
+ to pick items (see Axiom of Choice)
+
+- **Intuitionistic logic**, also called **constructive logic**: the new kid on
+ the block. In intuitionistic logic, we need to find a _witness_ for all of
+ our proofs. Also, falsehood is the absence of a witness, just like all the
+ stuff with the bottom type we just talked about, which models impossibility or
+ absurdity. In this logical system, the Axiom of Choice doesn't make any sense:
+ the act of proving that a choice exists involves generating an example of some
+ sort. Another notable difference is that intuitionistic does not consider the
+ Law of Excluded Middle to be true.
+
+However, intuitionistic logic is preferred in a lot of mechanized theorem
+provers, because it's easier computationally to talk about "having a witness".
+Let's actually look more closely at what it means to have a "witness".
+
+If you didn't read the section earlier about using private constructors to
+restrict type construction, I'm going to revisit the idea a bit here. Consider
+this very restrictive hash map:
+
+```ts
+namespace HashMap {
+ class Ticket {
+ /* ... */
+ } // Private to namespace
+
+ export class HashMap {
+ // ...
+
+ public insert(k: string, v: number): Ticket {
+ /* ... */
+ }
+
+ public getWithoutTicket(k: string): number | null {
+ if (!this.hasKey(k)) return null;
+ return this.inner[k];
+ }
+
+ public getWithTicket(t: Ticket): number {
+ return this.inner[t.key];
+ }
+ }
+}
+```
+
+The idea behind this is kind of like having a witness. Whenever you insert
+something into the map, you get back a ticket that basically proves that it was
+the one that inserted it for you in the first place.
+
+Since we used a namespace to hide access to the `Ticket` class, the only way you
+could have constructed a ticket is by inserting into the map. The ticket then
+serves as a _proof_ of the existence of the element inside the map (assuming you
+can't remove items).
+
+Now that we have a proof, we don't need to have `number | null` and check at
+runtime if a key was a valid key or not. As long as we have the ticket, it
+_guarantees_ for us that that key exists and we can just fetch it without asking
+any questions.
+
+In mechanized theorem provers,
+
+---
+
+To talk about that, we have to go back to treating types as sets. For example,
+we've already seen that the bottom type is a set with no elements, $\emptyset$.
+But what's a type that corresponds to a set with one element?
+
+In type theory, we call this a **unit type**. It's only got one element in it,
+so it's not super interesting. But that makes it a great return value for
+functions that aren't really returning anything, but _do_ return at all, as
+opposed to the bottom types. Typescript has something that behaves similarly:
+
+```ts
+function returnUnit(): null {
+ return null;
+}
+```
+
+There's nothing else that fits in this type. (I realize `void` and `undefined`
+also exist and are basically single-valued types, but they have other weird
+behavior that makes me not want to lump them in here)
+
+Let's just also jump into two-valued types, which in math we just call
+$\mathbf{2}$. This type has a more common analog in programming, it's the
+boolean type.
+
+Do you see how the number of possible values in a type starts to relate to the
+_size_ of the set now? I could go on, but typically 3+ sets aren't common enough
+to warrant languages providing built-in names for them. Instead, what languages
+will do is offer _unions_, which allow you to create your own structures.
+
+For example, let's try to create a type with 3 possible values. We're going to
+need 3 different unit types such that we can write something like this:
+
+```ts
+type Three = First | Second | Third;
+```
+
+We can just do three different unit classes.
+
+```ts
+class First {
+ static instance: First = new First();
+ private constructor() {}
+}
+class Second {
+ /* ... */
+} // same thing
+class Third {
+ /* ... */
+} // same thing
+```
+
+The reason I slapped on a private constructor and included a singleton
+`instance` variable is to ensure that there's only one value of the type that
+exists. Otherwise you could do something like this:
+
+```ts
+let first = new First();
+let differentFirst = new First();
+```
+
+and the size of the `First` type would have grown beyond just a single unit
+element.
+
+But anyway! You could repeat this kind of formulation for any number of
+_finitely_ sized types. In the biz, we would call the operator `|` a
+**type-former**, since it just took three different types and created a new type
+that used all three of them.
+
+[proposition]: https://en.wikipedia.org/wiki/Propositional_calculus
+[typescript]: https://www.typescriptlang.org/
+[never]: https://www.typescriptlang.org/docs/handbook/2/functions.html#never
+[false]: https://en.wikipedia.org/wiki/Principle_of_explosion
+[as]: https://www.typescriptlang.org/docs/handbook/2/everyday-types.html#type-assertions
+[//]: https://code.lol/post/programming/higher-kinded-types/
+[//]: https://ayazhafiz.com/articles/21/typescript-type-system-lambda-calculus
diff --git a/src/content/posts/2023-04-21-proving-true-from-false.lagda.md b/src/content/posts/2023-04-21-proving-true-from-false.lagda.md
new file mode 100644
index 0000000..416afe9
--- /dev/null
+++ b/src/content/posts/2023-04-21-proving-true-from-false.lagda.md
@@ -0,0 +1,170 @@
+---
+title : "Formally proving true ≢ false in cubical Agda"
+slug : "proving-true-from-false"
+date : 2023-04-21
+tags : ["type-theory", "agda"]
+math : true
+---
+
+
+Imports
+
+These are some imports that are required for code on this page to work properly.
+
+```agda
+{-# OPTIONS --cubical #-}
+
+open import Cubical.Foundations.Prelude
+open import Data.Bool
+open import Data.Unit
+open import Data.Empty
+
+¬_ : Set → Set
+¬ A = A → ⊥
+
+infix 4 _≢_
+_≢_ : ∀ {A : Set} → A → A → Set
+x ≢ y = ¬ (x ≡ y)
+```
+
+
+The other day, I was trying to prove `true ≢ false` in Agda. I would write the
+statement like this:
+
+```
+true≢false : true ≢ false
+```
+
+For many "obvious" statements, it suffices to just write `refl` since the two
+sides are trivially true via rewriting. For example:
+
+```
+open import Data.Nat
+1+2≡3 : 1 + 2 ≡ 3
+1+2≡3 = refl
+```
+
+This is saying that using the way addition is defined, we can just rewrite the
+left side so it becomes judgmentally equal to the right:
+
+```
+-- For convenience, here's the definition of addition:
+-- _+_ : Nat → Nat → Nat
+-- zero + m = m
+-- suc n + m = suc (n + m)
+```
+
+- 1 + 2
+- suc zero + suc (suc zero)
+- suc (zero + suc (suc zero))
+- suc (suc (suc zero))
+- 3
+
+However, in cubical Agda, naively using `refl` with the inverse statement
+doesn't work. I've commented it out so the code on this page can continue to
+compile.
+
+```
+-- true≢false = refl
+```
+
+It looks like it's not obvious to the interpreter that this statement is
+actually true. Why is that
+
+## Intuition
+
+Well, in constructive logic / constructive type theory, proving something is
+false is actually a bit different. You see, the definition of the `not`
+operator, or $\neg$, was:
+
+```
+-- ¬_ : Set → Set
+-- ¬ A = A → ⊥
+```
+
+> The code is commented out because it was already defined at the top of the
+> page in order for the code to compile.
+
+This roughly translates to, "give me any proof of A, and I'll produce a value of
+the bottom type." Since the bottom type $\bot$ is a type without values, being
+able to produce a value represents logical falsehood. So we're looking for a way
+to ensure that any proof of `true ≢ false` must lead to $\bot$.
+
+The strategy here is we define some kind of "type-map". Every time we see
+`true`, we'll map it to some arbitrary inhabited type, and every time we see
+`false`, we'll map it to empty.
+
+```
+bool-map : Bool → Type
+bool-map true = ⊤
+bool-map false = ⊥
+```
+
+This way, we can use the fact that transporting
+over a path (the path supposedly given to us as the witness that true ≢ false)
+will produce a function from the inhabited type we chose to the empty type!
+
+```
+true≢false p = transport (λ i → bool-map (p i)) tt
+```
+
+I used `true` here, but I could equally have just used anything else:
+
+```
+bool-map2 : Bool → Type
+bool-map2 true = 1 ≡ 1
+bool-map2 false = ⊥
+
+true≢false2 : true ≢ false
+true≢false2 p = transport (λ i → bool-map2 (p i)) refl
+```
+
+## Note on proving divergence on equivalent values
+
+Let's make sure this isn't broken by trying to apply this to something that's
+actually true:
+
+```
+data NotBool : Type where
+ true1 : NotBool
+ true2 : NotBool
+ same : true1 ≡ true2
+```
+
+In this data type, we have a path over `true1` and `true2` that is a part of the
+definition of the `NotBool` type. Since this is an intrinsic equality, we can't
+map `true1` and `true2` to divergent types. Let's see what happens:
+
+```
+notbool-map : NotBool → Type
+notbool-map true1 = ⊤
+notbool-map true2 = ⊥
+```
+
+Ok, we've defined the same thing that we did before, but Agda gives us this
+message:
+
+```text
+Errors:
+Incomplete pattern matching for notbool-map. Missing cases:
+ notbool-map (same i)
+when checking the definition of notbool-map
+```
+
+Agda helpfully notes that we still have another case in the inductive type to
+pattern match on. Let's just go ahead and give it some value:
+
+```text
+notbool-map (same i) = ⊤
+```
+
+If you give it `⊤`, it will complain that `⊥ != ⊤ of type Type`, but if you give
+it `⊥`, it will also complain! Because pattern matching on higher inductive
+types requires a functor over the path, we must provide a function that
+satisfies the equality `notbool-map true1 ≡ notbool-map true2`, which unless we
+have provided the same type to both, will not be possible.
+
+So in the end, this type `NotBool → Type` is only possible to write if the two
+types we mapped `true1` and `true2` can be proven equivalent. But this also
+means we can't use it to prove `true1 ≢ true2`, which is exactly the property we
+wanted to begin with.
diff --git a/src/content/posts/2023-05-06-equivalences.lagda.md b/src/content/posts/2023-05-06-equivalences.lagda.md
index 342acd9..74ce698 100644
--- a/src/content/posts/2023-05-06-equivalences.lagda.md
+++ b/src/content/posts/2023-05-06-equivalences.lagda.md
@@ -3,9 +3,9 @@ title: "Equivalences"
slug: "equivalences"
date: 2023-05-06
tags:
- - type-theory
- - agda
- - hott
+- type-theory
+- agda
+- hott
math: true
draft: true
---
@@ -58,7 +58,6 @@ we can just give $y$ again, and use the `refl` function above for the equality
proof
```
-
```
The next step is to prove that it's contractible. Using the same derivation for
@@ -149,9 +148,9 @@ Blocked on this issue: https://git.mzhang.io/school/cubical/issues/1
Now we can prove that the path is the same
\begin{CD}
-A @> > > B \\\
- @VVV @VVV \\\
- C @> > > D
+ A @> > > B \\\
+ @VVV @VVV \\\
+ C @> > > D
\end{CD}
- $A \rightarrow B$ is the path of the original fiber that we've specified, which is $f\ x \equiv y$
@@ -166,12 +165,10 @@ Bool-id-is-equiv .equiv-proof y .snd y₁ i .snd j =
c-d = y₁ .snd
in
?
-```
+ ```
Blocked on this issue: https://git.mzhang.io/school/cubical/issues/2
-
-```
-
+ ```
```
## Other Equivalences
diff --git a/src/content/posts/_index.md b/src/content/posts/_index.md
new file mode 100644
index 0000000..42545d4
--- /dev/null
+++ b/src/content/posts/_index.md
@@ -0,0 +1,7 @@
++++
+title = "Blog"
+weight = 1
+
+[cascade]
+type = "posts"
++++
diff --git a/src/data/links.ts b/src/data/links.ts
new file mode 100644
index 0000000..7e88ffb
--- /dev/null
+++ b/src/data/links.ts
@@ -0,0 +1,47 @@
+export interface Link {
+ name: string;
+ url: string;
+ icon: string;
+ description: string;
+}
+
+const links: Link[] = [
+ {
+ name: "Forgejo",
+ url: "https://git.mzhang.io",
+ icon: "gitea",
+ description: "Check out my public open source projects on Forgejo",
+ },
+ {
+ name: "Matrix",
+ url: "https://matrix.to/#/@michael:chat.mzhang.io",
+ icon: "matrix-org",
+ description: "Come chat with me on Matrix",
+ },
+ {
+ name: "GitHub",
+ url: "https://github.com/iptq",
+ icon: "github",
+ description: "See a history of my old projects on GitHub",
+ },
+ {
+ name: "Mastodon",
+ url: "https://fosstodon.org/@mzhang",
+ icon: "mastodon-square",
+ description: "Follow my ramblings on Mastodon",
+ },
+ {
+ name: "Keybase",
+ url: "https://keybase.io/michaelz",
+ icon: "keybase",
+ description: "Verify my other identities on Keybase",
+ },
+ {
+ name: "LinkedIn",
+ url: "https://linkedin.com/in/mzhang0",
+ icon: "linkedin",
+ description: "Connect with me on LinkedIn",
+ },
+];
+
+export default links;
diff --git a/src/layouts/BaseLayout.astro b/src/layouts/BaseLayout.astro
index 3b95ba7..625b3b0 100644
--- a/src/layouts/BaseLayout.astro
+++ b/src/layouts/BaseLayout.astro
@@ -1,4 +1,5 @@
---
+import Footer from "../components/Footer.astro";
import LeftNav from "../components/LeftNav.astro";
import "../styles/global.scss";
---
@@ -9,32 +10,19 @@ import "../styles/global.scss";
Michael Zhang
-
-
-
+