几天前看到了 Tsoding 的一段视频：Self-Reproducing Programs ，里面提到了 C 和 Rust 语言编译器的自举以及 Quine。这让我联想到了在《理论计算机科学导论》这门课上学到的 Y Combinator 和 Self-Printing Turing Machine 等内容。

感觉 Quine 是很有意思的一件事儿，但上次接触相关内容已经过了接近两年了，我早就把这些内容忘光了。于是又重新学习了相关资料，写下了这篇博客。

阿里云上已经不再提供原来的有效期为 12 个月的免费 SSL 证书了，有效期缩短为 90 天。也就是说，每隔 3 个月就需要重新申请一次。这就无可避免地需要在服务器上配置证书，于是我写下这篇文章，记录一下申请 SSL 证书的过程，以后就直接参考这篇文章的流程和代码即可。

班上准备参评校优秀班集体了，于是整理了一下自己大学以来的各类成就，顺便发在博客上以作记录。

2025 年 8 月 25 日 21:30 左右，我在北体育馆和计算机系篮球队的朋友们、还有几位五字班新生一起打球，结果不小心把左手弄骨折了。

由于这是我第一次（希望也是最后一次）骨折、（在我有意识的情况下的）第一次手术，因此我准备以博客的形式将此经历记录下来：一方面是作为一段酸甜的记忆给未来的自己回顾；另一方面，我希望分享我的就医流程，也许这能为其他同学提供一些帮助。

主要学习了“差分分析及其自动化”这个领域内的两篇论文：

• Differential and Linear Cryptanalysis Using Mixed-Integer Linear Programming，论文链接
• Automatic Security Evaluation and (Related-key) Differential Characteristic Search: Application to SIMON, PRESENT, LBlock, DES(L) and Other Bit-oriented Block Ciphers，ASIACRYPT 14'，论文链接

这学期在学习《操作系统》这门课程，参加了“操作系统大实验”来替代考试。我选择的方向是用形式化验证工具来验证 OS 的正确性，因此来学习一下 Kani。

这是 2025 春夏季开源操作系统训练营（第三阶段）的题解。

TL;DR：用形式化语言理解 OS——OS 是一个管理状态机的系统。

ATC'23, 论文链接