VeriSMo 的可信基只包括硬件和它自己（VM），剔除了对于 Hypervisor 的信任。传统的 VM 的安全服务是由 Hypervisor 负责的，如果认为 Hypervisor 是不可信的，那么就不能由它来提供安全服务。AMD 提供了新的安全架构 SEV-SNP，它为在 VM 中独立实现安全服务提供了支持，VeriSMO 就利用了这个硬件特性。

除了利用新的硬件安全特性外，VeriSMo 在开发时完成了形式化验证来确保安全性。VeriSMo 的开发语言是 Rust，已经确保了部分的内存安全性（也就是 Rust Checker 承担了部分形式化验证的任务），距离完全的形式化验证还有两个挑战：

1. 因为 Hypervisor 不可信任，所以 Hypervisor 可以打断 VM 的执行并修改硬件状态，这种并行无法简单验证。
2. 开发 VeriSMo 需要使用 Unsafe Rust，Rust Checker 无法验证这种情况。

为了解决挑战 1，VeriSMo 将验证拆分成了 2 层，上层为机器模型层（Machine Model），用 model verify 专门约束 Hypervisor 的行为，下层为实现层（Implement），用于解决排除了 Hypervisor 干扰后的 VeriSMo 本身的验证问题。

一、安全目标

1.1 总论

系统安全有 3 个目标：

• 机密性（Confidentiality）：又称隐私性（Privacy），是指数据不能被未授权的主体窃取（即恶意读操作）。
• 完整性（Integrity）：是指数据不能被未授权的主体篡改（即恶意写操作）。
• 可用性（Availability）：是指数据能够被授权主体正常访问。

合称 CIA 。

一、总论

这篇文章是对于旋元佑语法俱乐部的一个注释总结。行文思路基本上和这本电子书的章节保持一致。

语法是对于语言的规律总结，这类似于物理是对于客观世界的规律总结。不过应当注意到，即使掌握了语法，也并不能短时间内提高英语水平，因为在语法的指导下使用语言，同样是一个需要习惯和精进的过程。这就像掌握了物理定律和物理满分之间依然存在很大差距一样。

旋老师的语法和我中学学过的语法并不一样，旋老师倾向于建立一种“大一统”的理论来解释所有的语言现象，而中学语法则更加繁杂和缺少一致性。在加上我这次学习语法已经是大四，在逻辑思维上相比于中学已经有了很大的进步。所以总的来说，语法更加“讲理”了。

但是旋氏语法的缺点我个人感觉有两个，一个是因为过于“统一”，导致需要引入一堆与中学语法似是而非的概念，这些概念类似于物理学上的“波粒二象性”一样，对中学语法是一种挑战；并且因为旋老师是台湾人的缘故，所以在表达习惯和方式上也与大陆存在一定的差异（也就是他写的中文有点难看懂）。另一个是旋老师在建立了“统一”的理论后，并没有充分利用这些规律推导出中学语法甚至是其他中学语法难以推导的其他语言现象。

对于“死猪不怕开水烫”这句话，似乎每个人的理解是不同的：

有的人是“小太爷告诉你，咱得是猪，可不是那鸡鸭的便宜玩意儿”；

有的人是“跟嫩么说，别听前面的猪渍歪，介玩意儿就没带怕的”；

还有的人是“俺得用开水，不是开水可不瞻”。

但是很少有人想过”为什么我是死猪，为什么要用开水烫我“。

一、观感

天津真的很像十年前的石家庄。我指的不是发展程度，而是市容市貌。在街上随处可见将背心挽到胸口的大爷，拿着火钳子捅咕炉子，炭火上是一两只烤鸡翅或者烤虾。旁边的饭店有踩着趿拉板儿的姐姐拎着水管往街上滋着黑水。一个个脸上都是泥渍和晒疮的小孩子，将砖头揉碎了倒到书包里，两三个人拥着一辆比人都高的华丽的变速自行车，向着挤满三轮的岔路口奔去。而石家庄，可能是因为我不常回家的缘故，早已昏沉沉地睡去。

这是西北角的景象，而在五大道，我见过了最新奇的建筑群，洋房子里长出了商户，丝毫没有嫁接或者“捏到一起”的感觉。秃头或者蓬蓬头的胖大妈从一个漂亮的西式木头窗后探出头，这如果不是发生在天津，又能发生在哪里？

来到天津以后，我才感觉到，似乎我的一部分是在天津的。这个地方没有小红书上说得那么俏皮或者幽默，而更像是我小时候读到的《神鞭》一样，这里的人为了某种传统的生活方式，而憋着一口气，他们迫不及待地向别人证明，更向自己证明，我们这么活没有错。

一、编码

此章的目的是弄清楚 ASCII, GBK, Unicode, UTF-8 编码的区别，大部分知识都来源于这里。所以我只是简单转述一下：

ASCII 是最为古老的编码方式，它指的是用一个字节也就是 8 bit 完成编码，实际上只用了 7 bit ，最高位的值衡为 0 （这也成了其他编码方式兼容 ASCII 的一个重要抓手）。也就是说，ASCII 只能编码 2⁷ = 128 个文字，这对英文这种只有 26 个字母的语言体系是足够的。

但是 ASCII 并不能满足很多类似英语的语言体系，比如说 é, ג 这种字符都是原有的 ASCII 所没有的，但是幸运的是，很多语言的字符数本来就不多，比如俄语是 33 个，而法语是基础的 26 个英文字母加音标。所以这些语言同样可以用一个字节进行编码，英语字符占据了 0 ~ 127 ，它们就占据了 128 ~ 255 。这样的缺点就是不同国家的 128 ~ 255 表示不同的字母，彼此之间并不兼容。

但是像汉语这样的语言就没有那么轻松了，他们就算占据了 128 ~ 255 位，也最多增加 128 个字符，这对于有 10 万个字符的汉语来说是杯水车薪。所以中国就开发了 GB2312 编码系统，后来演变成了 GBK 系统。总的来说，就是采用两个 128 ~ 255 的字节来表示一个汉字（应该是差不多），这样的话大约可以表示 2 万多个汉字，但是这样其实有一些生僻一些的字也是无法表示的。

TCCL: 为 PCIe GPU 集群发现更好的通信路径

论文地址：https://dl.acm.org/doi/10.1145/3620666.3651362

项目地址：https://github.com/mcrl/tccl

一、背景

1.1 计算集群