Research
Delegation vs Review：你能交出去的，只有你能验证的
AI 写代码、找漏洞的速度，已经比人认真看的速度快了。一条条 review 看不过来以后，我们到底还能相信什么？这份信任又该划到哪里为止？ 阅读更多 →
鸡头学(Gitalogy)
鸡头学源自于一句俗语，“宁做鸡头，不做凤尾”。本学科的基础理论基本来自于作者对于身边的鸡头，鸡屁股，以及想要成为鸡头的各种人和事情的观察。 阅读更多 →
GPU在Confidential Computing中如何管理内存？
从UVM分配开始 Path: kernel-open/nvidia-uvm/uvm_va_space.c 注意这个： if (uvm_conf_computing_mode_enabled(gpu)) { NvU32 gpu_index = uvm_id_gpu_index(gpu->id); status = … 阅读更多 →
摄影和科研
最近重新拾起了相机，惊觉摄影和科研（至少在计算机领域）简直相似地过分。强烈建议学术民工尝试一下摄影，或者摄影师尝试一下科研（？）。 阅读更多 →
GPUTEE从入门到升天（尚未升天）
从零开始一个H100 GPUTEE的配置，顺便体会做Artifact Evaluation的痛苦。这里主要记录踩坑，文档里面有的东西不再赘述。我对于VM和GPU的知识基本等于空白，搞了两天终于卡在了需要NVIDIA支持的地方上了。 阅读更多 →
Verifying Constant-time
Constant-time的验证方法们。 Intro Constant-time作为密码学实现上一个重要的property，在抵御side-channel上面有很重要的作用。尤其是在这个Post-spectre的年代，microarchitectural level的side-channel attack已经成为了一个很大的威胁。近年来这个领域的researcher们飙了很多关于constant … 阅读更多 →
学术相关，每月Check！
Academic Conferences Mainly focus on Security, System & PL. Security Top Tier NDSS, Mar. SP, May Security, Aug. CCS, Nov. Great Ones Euro SP, July Asia CCS, June DSN, June ACSAC, Dec. ESORICS, … 阅读更多 →
SMT/SAT从0到0.1
最近在学习一些关于SMT/SAT solver的东西，在这里简单总结一下。 概念 SMT: satisfiability modulo theories；wiki SAT: (boolean) satisfiability wiki SMT可以认为是SAT的泛化。SAT基本只限制在求解boolean的一个表达式的satifiability上，即（是否有）赋值使得一个表达式为真(SAT)。 如若不存 … 阅读更多 →
符号和解释
在被Coq折磨了快一个月后，终于我终于看完了Logic Foundation。作为Software Foundations系列书籍中的第一员大将，它还是有点东西的。这里只浅谈一下我对于符号和解释这两个概念所产生的更深的理解。正文部分基本不涉及任何与编程本身相关的问题。 阅读更多 →
关于博客的一些变化
最近好像博客都没啥更新，但其实不是的：我用上了TiddlyWiki作为自己的笔记本。 阅读更多 →