近日,被誉为全球计算机系统领域“奥运会”的顶级学术会议SOSP 2025公布奖项评选结果,“星绽”开源操作系统在高可扩展内存管理方面的研究论文,斩获今年的最佳论文奖(Best Paper Award)。据悉,本届SOSP会议共收到368篇投稿,最终录用66篇,其中最佳论文奖仅设三席。这标志着星绽OS在破解操作系统“性能与安全兼顾”这一难题上的探索,获得了国际学术界的认可。
“星绽”(Asterinas)是由中关村实验室、蚂蚁集团、北京大学、南方科技大学等机构联合发起,并在2024年10月22日向全球开发者开源,聚焦于安全可信底层技术的开源系统软件栈。星绽系统软件栈包括星绽OS、星绽机密计算两大项目,其中星绽OS内核作为下一代工业强度的开源通用OS内核,兼顾性能和安全,采用首创的框内核架构和新兴的Rust编程语言,支持x86和RISC-V等CPU体系架构,不仅兼容Linux内核,还在安全性方面有望大幅领先于Linux和其他现有主流OS。

据悉,SOSP始于1967年,与它的姊妹会议OSDI 一起,被全球学术界和工业界公认为操作系统和系统软件领域最高水平、最权威、最具影响力的顶级会议,被称为计算机系统领域的“奥运会”。SOSP/OSDI也深受全球科技公司的重视,Google、Microsoft、Meta、Amazon、Apple等科技公司会派遣核心研发人员参会、投稿及做报告等。许多在工业界产生巨大影响的项目,其核心论文都发表在SOSP/OSDI上。目前,SOSP/OSDI已经成为衡量一个研究机构或团队在系统领域是否处于世界领先水平的关键标尺,是孕育颠覆性计算技术的摇篮。
现代内存管理系统长期存在的两大痛点:性能瓶颈与并发安全。本次获奖论文《CortenMM: Efficient Memory Management with Strong Correctness Guarantees》,阐释了星绽操作系统的独创技术CortenMM在这一领域的探索。该文由北京大学、中关村实验室、蚂蚁集团、CertiK公司、加州大学洛杉矶分校、密歇根理工大学等共同合作完成。
论文提出,传统操作系统如Linux普遍采用“软件—硬件”两级抽象设计,好处是在很大程度上保证了操作系统在不同硬件平台之间的可移植性,但显著的同步开销严重制约多核处理器的性能发挥,而潜在的并发漏洞则带来安全风险。
研究团队发现,x86、ARM和RISC-V等几种主流指令集架构在其内存管理单元(MMU)的设计上已经趋于统一,因此过去为屏蔽硬件差异而存在的软件抽象层已不再是必需品。基于这一关键判断,星绽创新成果CortenMM摒弃了独立的软件抽象层,实现了一种“单层抽象”的全新系统架构,使应用程序能直接与经过硬件强化的接口进行交互。
CortenMM的简化设计带来了显著的性能提升,其同步正确性也得到了研究验证。通过消除软件层的额外同步开销,CortenMM的性能得到释放,在真实应用场景下,性能最高可达Linux的26倍。通过创新性地引入统一的事务化接口(Transactional Interface),利用Rust语言自身的安全特性,并结合先进的形式化验证工具(Verus)进行严格推演,研究团队成功证明了CortenMM核心并发代码的正确性,从根本上杜绝了复杂的并发漏洞。
2024年10月,“星绽”对外发布并向全球开发者开源。一年来,星绽开源操作系统三篇论文被顶会收录,除了CortenMM的研究论文入选SOSP 2025外,星绽两篇论文被顶级会议USENIX ATC 2025同时录用。此外,星绽在GitHub平台斩获逾3600颗Star,并登上HackerNews和LWN.net等国外主流技术社区头条,获2025年OS2ATC大会“最具影响力开源创新贡献奖”。
好文章,需要你的鼓励
企业AI搜索公司Glean宣布年度经常性收入(ARR)达3亿美元,较15个月前的1亿美元增长三倍。尽管谷歌、微软、OpenAI等科技巨头纷纷入局企业AI搜索市场,Glean凭借"上下文图谱"技术深度理解企业业务需求,并帮助客户显著降低AI计算成本。该公司提供按用量计费和混合定价两种模式,客户涵盖Databricks、Reddit、Pinterest及三星等企业。Glean上轮融资后估值达72亿美元。
香港中文大学与MiniMax提出ClaimDiff-RL框架,将图像描述的AI训练从整体打分升级为逐条核查,有效解决了传统方式导致AI"少说保平安"的问题,同时在多项基准测试上超越Gemini-3-Pro-Preview。
杰夫·贝索斯旗下的蓝色起源公司在佛罗里达卡纳维拉尔角进行静态点火测试时,新格伦重型火箭发生爆炸。这是美国历史上最大规模的火箭爆炸之一,也是蓝色起源公司遭遇的最严重失败。所有人员安全,但该事故可能导致新格伦火箭项目长期暂停。此前该火箭已成功完成三次发射,并实现了助推器回收和重复使用。
ParaVT是一个由南洋理工等多校联合提出的并行视频工具调用框架,通过让AI同时分析多段视频并引入PARA-GRPO算法解决训练中的格式崩溃与工具跳过问题,在六项长视频理解测试中平均提升约7.9%。