CS
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支持的地方上了。 参考资料 Confidential Computing Deployment Guide CUDA Installation Guide GitHub: AMDSEV … 阅读更多 →
Verifying Constant-time
Constant-time的验证方法们。 Intro Constant-time作为密码学实现上一个重要的property，在抵御side-channel上面有很重要的作用。尤其是在这个Post-spectre的年代，microarchitectural level的side-channel attack已经成为了一个很大的威胁。近年来这个领域的researcher们飙了很多关于constant … 阅读更多 →
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系列书籍中的第一员大将，它还是有点东西的。这里只浅谈一下我对于符号和解释这两个概念所产生的更深的理解。正文部分基本不涉及任何与编程本身相关的问题。 Preface 我并不打算对书的中知识概括总结，而是希望浅谈自己在读书过程中对于两个重要的概念，符号与解释的一些理解和思考。 在这 … 阅读更多 →
从零开始搓一个编译器
今年手痒痒选了一个Implementation of PL的课，需要徒手搓编译器。这里来小记一下这个过程，感觉这可能是我校CS最硬核的课之一了。 其实老师给了Racket和Python两种语言的选择，奈何我实在是不习惯那长到姥姥家的Racket括号，于是选择了Python。幸好在最新的Python 3.10中引入了match case的新特性，这直接使得代码量减少了非常多！它太好用了！！！（感 … 阅读更多 →
计算机玄学——主要是踩的Rust的坑
有言道： 我的一生， 是和Rust Compiler搏斗的一生。 ——我 又有言道： 当你觉得Rust出现问题， 不是因为Rust有问题， 而是，你有问题。 ——还是我 CString Ownership 最近在做Teaclave的开发，使用到了很多FFI的玩意。但是CString却给我留下了深刻的印象。 Problem NativeSymbol { symbol: … 阅读更多 →
计算机玄学——主要是踩的C的坑
计算机没有玄学，因为它没有血肉。 但凡认为计算机玄学存在者皆是麻瓜。 ——我 cdqe 现象 和儿子debug的时候遇到了计算机玄学问题： syscallnr = rec->nr; printf("syscallnr=%d\n", syscallnr); //WL: debug printf("In renderxxx\nsyscall table address: … 阅读更多 →
Rust 学习笔记
最近突然对于Rust产生了兴趣因为它的吉祥物小螃蟹很可爱，遂开始阅读The Rust PL一书想要一探究竟。我发现Rust真的是一门相当阳间的语言，一些functional programming的特性和build system可以让使用者用起来十分舒爽。 虽然目前只看了两十章，但我已经从代码中嗅到了了浓郁的Rust的香锈味。 基本看完了现在。 在一个较为清闲的周末早上，我决定把最后一章看完。 创 … 阅读更多 →
Programming Language Review
Review what I learned from programming language, a fundamental course of CS. The code is mainly in typed racket, a dialect of scheme. The code here is mainly from Weixi Ma’s lecture notes and my … 阅读更多 →