剑桥大学计算机实验室

剑桥大学计算机实验室，全球历史最悠久、最负盛名的计算机科学系之一，自 1937 年起开展计算科学的先驱研究。

训练 Tessera 地空间基础模型中获得的运行型 HPC 经验 [pdf]

剑桥大学团队发布 Tessera 地空间基础模型系列的 HPC 运维报告。Tessera 将 Sentinel-1/2 时间序列压缩为全球 10m 像素的年度嵌入，已在生态、农业、气象等任务中广泛使用，推理产物达到 PB 级。团队从剑桥自有 Intel Dawn 集群起步，先后接入 AMD MI300X/MI325X 开发者云、NVIDIA Isambard GH200 512 卡分配和 Zenith MI355X 预览系统，记录了一次次跨厂商迁移中的实际收益与坑点：Intel GPU 默认八逻辑设备调度易碎、oneCCL IPC 不可靠、ROCm 2 小时起环境、torch.compile 加速 1.46–1.60 倍、源卫星数据带宽成为推理瓶颈、Isambard 24 小时任务限制拖累长期训练、ARM64 NCCL 偶发挂起。报告最终提出六项面向研究计算者的跨厂商建议，包括预装验证过的 PyTorch+MPI 镜像、版本化容器、预留多日窗口等。对关注 HPC、GPU 异构训练与大规模地理数据管道的工程师和研究者有直接参考价值。

收藏4 小时前

X11 的 Unicode 字体与工具

Markus Kuhn 维护的经典 X11 Misc-Fixed 位图字体系列已扩展为完整 ISO 10646-1/Unicode 3.2 版本。涵盖从 5x7 到 10x20 共十余种尺寸，支持 ISO 8859 全系列、CP437/1251/1252、WGL4、KOI8-R、DEC VT100 图形符号等字符集；其中 6x13、8x13、9x15、10x20 等大尺寸字体还覆盖国际音标、亚美尼亚文、格鲁吉亚文、泰文、意第绪文、全部数学符号（含 TeX 全集）、APL、盲文、卢恩文乃至埃塞俄比亚文。新增斜体变体（6x13O/7x13O/8x13O）、9x18 改进版字形及日韩双宽汉字字体。Adobe/B&H 像素字体也已更新，修复了缺失 NBSP、乘除号互换等长期 bug。附下载链接和转换脚本，已被 XFree86 4.1 收录。

收藏117 天前

代码-规约-测试-调试-证明：将分离逻辑规约灵活融入常规开发工作流

本论文提出代码-规约-测试-调试-证明的增量式工作流，将分离逻辑规约融入常规C语言开发流程，在Google Android pKVM虚拟化监视器的生产级内存分配器上找到4个真实bug。传统形式化验证需与代码同步开发规约，难以适配已有系统。作者开发了CN规约语言及配套工具链：Fulminate运行时断言检查、Darcy属性基测试及CN形式化证明，支持先通过轻量级运行时检查快速迭代规约，再用属性基测试充分验证，最后在规约成熟后进行机器检查证明。该工作以真实生产代码验证了测试优先的规约开发方法，弥合了测试社区与证明社区之间的长期隔阂，为形式化验证的大规模实用化提供了可行路径。

收藏133 天前

可信计算常见问题解答（2003年版）

剑桥大学安全泰斗Ross Anderson于2003年撰写的经典FAQ，核心看点：在可信计算尚未大范围落地时，就精准预言了DRM强制执行、远程内容撤销、软件租赁、平台锁定、数字审查等一系列后来真实上演的博弈。文章从Fritz芯片的启动度量链讲起，逐一拆解TCPA/Palladium的技术机制——硬件如何向内容商证明环境"可信"、密钥如何仅在授权应用存活期间可用、远程黑名单如何让盗版文件在全球范围内无法打开。不止于技术，作者把视角拉到Gutenberg印刷术以来的信息自由传统，指出一旦单一权力机构控制Fritz芯片的认证与撤销，censorship将从法院延伸到每一台PC。还分析了Intel与Microsoft的商业动机、对竞争生态的扼杀效应、以及对吹哨人和政治异见者的威胁。至今仍是理解平台信任、DRM与数字主权争论绕不开的深度文献，观点鲜明、论证扎实、信息密度极高。

收藏142 天前

ASCII与Unicode引号使用规范

经典技术参考：剑桥学者Markus Kuhn详细解释为何不应将ASCII反引号(0x60)当作左引号、撇号(0x27)当作右引号。文章涵盖历史背景——老版X Window字体错误地将0x60/0x27渲染为左右方向引号，而现代Unicode/ISO标准要求专用字符U+2018/U+2019等；PostScript不同编码向量的映射混乱；TeX字体限制；以及实用修复指南（grep查找、perl替换）。作者本人深度参与了X核心字体的修订，内容权威、细节丰富、证据确凿，是程序员和排版爱好者绕不开的经典参考文。

收藏198 天前

UTF-8 诞生史（2003）

Rob Pike 本人亲述：广为流传的"IBM 设计 UTF-8、Plan 9 实现"是错误版本。真实故事发生在 1992 年 9 月某个夜晚，Ken Thompson 和 Rob Pike 在新泽西一家餐馆的餐垫上当场设计出了 UTF-8。当时 X/Open 委员会请他们评审 FSS/UTF 方案，两人发现该方案缺乏"任意位置切入字节流可同步"这一关键特性，于是趁晚餐机会重新设计，Ken 解决了位填充算法。当晚回到实验室后，Ken 连夜写打包/解包代码，Rob 修改 C 库和图形库，到周五 Plan 9 已全盘切换至 UTF-8。文章还附有 1992 年的原始邮件存档、两份提案的代码对照（含最早的 FSS/UTF 非自同步版本），以及 Ken 提交给 X/Open 的最终提案全文和 6 条设计准则。这是一份珍贵的技术史一手史料，纠正了 RFC2279 等后续文献中的错误记载。

收藏207 天前

The Global Trust Register (1999)

收藏223 天前

对信任的反思（1984年图灵奖演讲）

一篇经典计算机安全论文的课程导读。肯·汤普森（Ken Thompson）在1984年图灵奖演讲中展示了计算机安全史上最著名的思想实验：通过篡改编译器二进制，在系统源码完全不可见的情况下植入自我永续的后门。攻击分为三阶段——编写自打印程序、让编译器拥有源码中不存在的知识、利用编译过程自动注入并传递后门代码。最终整个操作系统的源码看起来干净，但运行二进制始终有毒。这篇导读来自剑桥大学计算机课程 R209，提供了论文背景、三阶段拆解、对当前系统的讨论问题（源码审计 vs 二进制审计、实用性、信任链的边界），并提及该思想最早可追溯至1974年美国空军对 Multics 的安全评估报告。适合安全从业者、编译器开发者及对供应链攻击感兴趣的技术读者。

收藏241 天前

带平滑闰秒的协调世界时 (UTC-SLS)

剑桥大学学者Markus Kuhn提出的一种优雅处理计算机系统闰秒问题的技术方案。传统UTC闰秒跳变会导致系统时钟不单调、引发分布式系统崩溃，UTC-SLS通过在闰秒前后1000秒内线性微调时钟速率（±0.1%），让应用层完全感知不到闰秒存在，从而隔离绝大多数开发者无需关心闰秒实现细节。文章详细给出了平滑规格、与Google"leap smear"方案在实现位置（NTP服务器端 vs 客户端/内核）和平滑函数形状（余弦 vs 线性）上的本质差异，并逐一回应了外界批评——包括为何不直接改用TAI、为何选择IETF而非ITU-R标准化。作者立场鲜明、逻辑严密，是一份有真实工程实践价值的技术提议，也保留了值得继续讨论的争议空间。

收藏245 天前

剑桥网络犯罪中心十年回顾（2025）

剑桥网络犯罪中心（CCC）发布十年回顾报告：该中心已从单纯的数据提供者演变为研究生态系统，通过开放CrimeBB（1.29亿条论坛帖子）、ExtremeBB（7150万条极端主义帖子）及Telegram/Discord聊天数据集，大幅降低了网络犯罪研究的准入门槛。报告基于203篇文献综述、44位用户调查和10组深度访谈，发现131篇论文直接使用了中心数据，覆盖31个国家473位学者，尤其在支持研究生和早期职业研究者方面效果显著——许多人表示没有CCC的数据，他们根本无法开展实证研究。 PostCog分析工具被证明是关键成功因素，既帮助社会科学研究者克服技术障碍，也被计算专家用于提效。中心正从传统论坛转向即时通讯平台，以追踪网络犯罪从论坛向聊天渠道迁移的趋势。报告也指出了数据许可流程繁琐、工具认知度不足等改进空间。

收藏252 天前

通信智能体的空间与运动

图灵奖得主Robin Milner的经典学术专著，提出"大图(bigraphs)"这一形式化模型，将空间中的放置关系与节点间的连接关系统一建模，用于描述普适计算系统中自治智能体的交互与动态重配置。书中从基本定义、代数结构到反应系统严谨推进，并演示了如何将CCS、Petri网等经典并发模型编码为特化的大图反应系统(BRS)。核心贡献在于为理解大规模自治系统的结构与行为提供了一个统一的理论框架，是进程演算与并发理论领域的重要参考文献。适合对形式化方法、普适计算建模有深入兴趣的学术读者。

收藏257 天前

使用CHERI能力为C和C++实现完整空间内存安全

剑桥大学博士论文，用CHERI纯能力（pure-capability）编程模型为C/C++提供字节级空间内存保护，堵住缓冲区溢出等内存漏洞的根源。作者设计并实现了完整方案：不仅保护语言可见指针，还保护函数调用、全局变量访问等隐式指针，并提出了CheriSH技术防止同一对象内字段间的越界。性能评估结果惊人——几何平均开销仅0.1%，最差情况23.3%，远优于大多数学术方案。更难得的是兼容性：移植PostgreSQL和WebKit只需修改不到0.1%的源代码行。结论是纯能力CHERI C/C++是一种可行的高安全编程环境，兼顾强内存保护、源码级兼容和低性能开销。适合对系统安全、编程语言底层机制和硬件安全扩展感兴趣的技术读者深入阅读。

收藏276 天前

The Quest to Replace Passwords: a comparative evaluation of Web authn schemes

收藏296 天前

为什么高阶逻辑是硬件描述与验证的良好形式化方法

这是一篇1985年剑桥大学Mike Gordon撰写的经典技术报告，核心论证高阶逻辑既能作为硬件描述语言，也能作为验证设计是否满足规格的形式化框架。报告通过CMOS反相器、全加器、行波进位加法器、时序乘法器和边沿触发D寄存器等多个电路实例，具体展示了规格描述和验证技术。对形式化验证和硬件设计领域有历史文献参考价值，但距今已近40年，技术内容多已融入后续教材和工具，对非专业读者缺少当下可用的实操或讨论入口。

收藏328 天前

人脸数据库

剑桥大学 AT&T 实验室 1992–1994 年收集的经典人脸识别数据集（原 ORL 数据库）。包含 40 位对象、每人 10 张不同光照/表情/面部细节的灰度图像（92×112 像素，PGM 格式），共 400 张。页面仅提供数据集结构说明、下载链接和使用引用要求，无任何分析、观点或讨论价值，属于纯粹的资源说明页。

收藏329 天前

显示器分辨率计算器：你的眼睛能分辨多少像素

你的显示器真的需要4K甚至8K吗？剑桥大学计算机实验室基于发表在《自然·通讯》上的人眼分辨率极限实测研究，推出了这个交互式计算工具。输入屏幕尺寸、分辨率、观看距离，即可算出你实际能用到的像素密度（每度像素数），以及多少人能看出当前显示器与“完美显示器”的差异。内置的“分辨率极限矩阵”图表直观显示了常见屏幕尺寸与距离下，95%的人已经无法分辨更高分辨率的临界点——超出那个值，画质不会再变清晰。背后有同行评审论文、开源代码和实测数据支撑，不是拍脑袋的公式，而是真正的视觉科学。适合挑选显示器、评估观看距离、或者单纯好奇“我的眼睛够不够用”的人点进去玩一玩。

收藏336 天前

编程语言与物理量纲

这是一篇1996年剑桥大学计算机实验室的博士论文技术报告，研究如何在编程语言中引入物理量纲（单位）的类型系统，使编译器能自动检查方程式量纲一致性。论文提出了类似ML的多态量纲类型系统及自动类型推理算法，并通过操作语义和指称语义严格证明了类型安全性。对编程语言研究者、类型系统爱好者有学术参考价值，但页面仅有摘要和PDF链接，无现场观察、个人观点或讨论入口，属于纯学术存档内容。

收藏415 天前

BCPL（2022年发布版）

BCPL编译器/解释器官方分发页面，由语言设计者马丁·理查兹本人维护。BCPL（1966年诞生）是早期无类型编程语言，深刻影响了B语言和C语言的发展。页面提供完整源码、安装说明、详细目录结构，包含32位/64位Cintcode解释器、演示程序、实验性本地代码移植及罕见的Windows CE版本支持。作者还特别提醒了浏览器自动解压.tgz文件导致的问题及处理技巧。对编程语言历史、编译器技术和复古计算领域有独特的一手资源价值。

收藏457 天前

SKIM：使用定制硬件实现函数式语言

这是1985年剑桥大学博士论文的技术报告，介绍作者为加速函数式程序求值而设计的专用处理器SKIM，涵盖组合子归约改进、director string实现方案以及函数式语言中I/O与非确定性任务的表示方法。全文需下载PDF查看。作为40年前的学术存档，内容已严重过时，缺乏当下讨论入口和实用价值，仅对编程语言历史研究有极小参考意义。

收藏481 天前

如何通过虹膜识别技术确认「阿富汗少女」的身份

虹膜识别算法发明人 John Daugman 亲述：他是如何用自己开发的 IrisCode 技术，确认国家地理标志性封面「阿富汗少女」的身份。1984 年拍摄的 12 岁难民女孩，18 年后在阿富汗偏远地区被重新找到，Daugman 将两张照片中的虹膜区域放大并编码比对，左眼汉明距离 0.24、右眼 0.31——不同虹膜出现如此低相似度的概率分别仅为 10^15 分之一和 600 万分之一。国家地理接受此结论并推出第二期封面，同时成立「阿富汗少女基金」支持穆斯林女童教育。文章附有原始处理图像、比对结果截图及虹膜识别原理论文链接，是一手技术细节与人文叙事兼备的经典案例。

收藏483 天前

英国警方数据库滥用案已占全国网络犯罪起诉半数以上

英国警方人员滥用内部数据库的案件，已占全国网络犯罪起诉案件半数以上——2024年上半年高达56%。剑桥大学网络犯罪中心主任Alice Hutchings基于其维护的英国网络犯罪数据库(CCCD)发布研究，曝光多起堪比电影情节的案例：有警察情报分析师向毒贩泄露加密通信平台行动信息，致跨国行动受损；有伦敦警察厅员工为帮谋杀犯找出关键证人身份，多次非法访问情报系统。论文追踪了从2010到2024年这一比例从34%飙升至56%的惊人趋势。作者尖锐指出：警方长期呼吁削弱加密以便获取公民通信数据，但内部数据滥用已证明现有政策失效；不解决有毒警察文化和有罪不罚心态，更多技术手段只会让问题恶化。这篇基于一手实证数据的论文，为反对削弱端到端加密提供了有力论据。

收藏578 天前

交互式定理证明的历史

三位领域内顶尖学者联手撰写的交互式定理证明权威历史综述。文章追溯了从1960年代Automath系统的诞生（de Bruijn独立重新发现Curry-Howard同构）、SAM系列半自动化证明器的演进，到现代Coq、Agda、NuPRL、LF框架等系统的技术脉络。详细梳理了自动定理证明与交互式证明的长期博弈：早期对全自动化的狂热、自动化能力的瓶颈、以及近年两者走向融合的趋势。包含Automath代码示例及类型推导的技术细节，对形式化验证、数学基础、编程语言理论领域的研究者极具参考价值。文风为标准的学术综述，客观中立，没有个人立场或争议性观点。

收藏580 天前