【免费下载链接】astridAstrid is a portable, capability-secure operating system for composable software.项目地址https://gitcode.com/gh_mirrors/astrid2/astrid点击查看免费下载导读本文是 Astrid 原生内核astrid-native-kernel架构决策记录的完整技术解读。Astrid 是一个便携、基于能力安全capability-secure的操作系统其原生内核是一个能力微内核唯一的产品是在相互不信任的保护域之间强制边界。本文以仓库中的 docs/astrid-kernel-adrs.md 为主体骨架系统讲解 Milestone 0 退出前必须落地的七项机制决策——保护域、能力对象表示、句柄转移、撤销、故障端点、调度、审计排序——并辅以 内核宪章、威胁模型、需求到证据矩阵 与仓库源码佐证。读完本文你将理解每一项 ADR 的上下文、决策、被否决的替代方案与后果掌握 Astrid 内核少量机制承载多属性的设计哲学以及这些决策如何映射为可验证的 REQ 证据条目。一、ADR 文档的定位约束内的具体选择Astrid 内核有一套分层文档体系各有分工内核宪章Charter设定不变量invariants哪些东西永远不许进入 ring 0ring 0 必须提供什么威胁模型Threat Model说明防御对象我们对抗什么、不宣称防御什么需求到证据矩阵Evidence Matrix说明每个声明如何被证伪一条属性没有可执行证据就不算持有原生内核范围Native Kernel Scope界定首台机器契约与执行计划AI 原生 OS 工作计划Workplan将上述文档转为带证据与退出条件的工作项其中明确要求记录保护域、能力对象表示、句柄转移、撤销、故障端点、调度、审计排序的 ADR。而ADR架构决策记录记录的是生活在这些约束内部的、具体的机制选择——即多个设计都能满足宪章、必须二选一的地方。每一份记录都写明上下文、决策、被权衡过的替代方案和后果让后来的读者不仅看到选了什么还看到否掉了什么、为什么。记录约定七个决策分别编号为ADR-K1至ADR-K7从 ABI 草图和证据矩阵行中引用ADR 只能通过宪章的修订程序charter §10变更替代它的 ADR 必须指名被替换的记录以及迫使变更的证据采用单一决策日志一份文件而非每条记录一个文件因为七项决策强耦合审阅者需要连在一起读若未来积累大量独立决策拆分为一记录一文件这件事本身也要走一次 ADR。与工作计划的对应关系工作计划的架构契约与可追溯性章节明确标记了以下交付物已完成[x]记录原生内核范围与显式非目标编写简明内核宪章Astrid Kernel Charter编写覆盖固件/虚拟机监控器/设备固件/恶意原生域/运行时宿主沦陷/恶意胶囊/恶意驱动/DMA/恢复基础设施的系统威胁模型Astrid Kernel Threat Model为每个声称的安全属性创建需求到证据矩阵Astrid Kernel Requirement-to-Evidence Matrix记录本篇文章主题的七项 ADR。二、ADR-K1保护域Protection domains上下文宪章§3规定一个域拥有页表、任务、能力表、预算和一个故障端点§2规定域比 POSIX 进程更小——没有 fork、用户、文件描述符或全局命名空间。首台机器是单 CPU范围文档 §6.2。仍待决定的是域的具体形态以及域是否嵌套。决策保护域是隔离与权力的单位由一个固定布局的内核对象表示持有页表根page-table root能力表ADR-K2调度上下文ADR-K6单个故障端点ADR-K5池计费账户pool-charge accountcharter §6。v0 内核中的域是单线程的——一个任务、一条指令流——这与单 CPU 机器契约吻合也与 Realm actor 模型单线程客户边界足以支撑第一套系统的既有验证一致。域不嵌套不存在父拥有子地址空间的包含关系。监督supervision是一种能力关系ADR-K5而非结构关系。init/恢复域只是普通域仅由测量引导计划measured boot plan赋予它的授权charter §7加以区分。被否决的替代方案方案否决理由(a) POSIX 进程形态的域线程、fd、命名空间被契约covenant否决——这正是宪章明确排除的表面(b) 嵌套域、分层地址空间所有权类 hypervisor 设计把故障树与权力树混为一谈宪章刻意把监督保持为能力而非包含关系嵌套还会让撤销完备性ADR-K4从扁平派生图退化为传递包含推理(c) v0 就支持多线程域推迟SMP 与域内并发是 scope-M7 关切现在接纳会迫使调度器与能力表在单 hart 边界被证明之前就变成并发结构后果对象定长、池分配对应证据REQ-MEM-1单线程域使能力表和故障处理在 v0 中无域内竞态未来多线程是对本 ADR 的增量修改而非重写——因为这里的单线程假设只在执行模型不在权力模型证据REQ-CAP-4清单声明永不是权力、REQ-MEM-4W^X 对全部域映射成立。三、ADR-K2能力对象表示Capability object representation上下文宪章要求不可伪造的每域句柄携带权限掩码rights mask与来源provenance转移时只允许收缩并同时支持范围撤销scoped与完整撤销completecharter §4、§7。两个成熟设计朝不同方向拉扯seL4 的 CNode 能力派生树CDT撤销通过遍历树实现EROS 的对象版本/分配计数计数加一即可 O(1) 使所有未决能力失效无需遍历。决策能力是域的定长能力表中的一个条目{ object handle, rights mask, derivation link }被引用的内核对象携带一个代计数器generation counter。能力条目仅当其记录代与被引用对象当前代相等时才有效——这是 EROS 洞见通过代递增generation bump实现 O(1) 的批量失效。对于范围撤销撤销派生自某能力的一切、但不销毁对象派生链接串联一条父→子图在僵尸/抢占点纪律ADR-K4下增量遍历。表索引不可伪造因为它永不是指针、永不离开内核用户空间只用表槽位table slot命名能力内核解析 slot→entry→代校验对象。被否决的替代方案方案否决理由(a) 纯 seL4 CDT作为唯一机制被否决整个对象销毁总是代价一次树遍历而常见情形域死亡、其对已销毁对象的所有能力都要消亡应当是 O(1)(b) 纯 EROS 代计数作为唯一机制被否决无法表达撤销某个子委托同时保住对象存活而宪章的衰减委托attenuated-delegation模型需要它(c) 稀疏能力 / 密码能力不可猜测比特串、无表被否决抵抗撤销与审计且宪章的可读性legibility要求把能力枚举为类型化关系每域表直接给出这一点后果每次能力使用付出一次代比较廉价每条目保留一个派生链接一个池槽域/对象死亡的批量失效为O(1)范围撤销是有界的遍历表本身就是可读性表面导出的基础关系charter §3所有者域、对象、权限、来源——无需独立存储REQ-LEG-1证据REQ-CAP-1句柄是不可伪造的每域表索引、REQ-CAP-2句柄转移只窄化权限、REQ-FAULT-2撤销完备性。四、ADR-K3句柄转移Handle transfer上下文能力通过 IPC 在域之间移动charter §4.2权限只许收缩转移必须显式且有界结果必须在序列化后依然有效charter §4.5使同一机制能跨未来的网络跳。决策转移是一个显式操作携带在有界、类型化的 IPC 消息中消息指名源槽位与权限掩码。内核在接收方表中创建新条目其权限为requested ∩ source绝不更多对象句柄与代复制自源派生链接指向源条目——扩展 ADR-K2 的图使被转移能力既可被对象代递增撤销也可被其祖先的范围撤销撤销。关键约束没有环境式或隐式转移消息未指名的能力不会被转移域不能转移它不持有的能力转移是派生derivation而非移动move源保留其能力除非它显式撤销自己的即 Realm 的 spawn 记录已在用的 dup 后关父形态。被否决的替代方案方案否决理由(a) 移动语义转移消费源作为默认被否决委托delegation而非交接handoff才是常见情形移动可表达为转移后撤销(b) 通过可信经纪商加宽权限彻底否决违反单调收缩不变量且模型中不存在足够可信的经纪商(c) 转移裸对象指针或地址被否决指针无法跨序列化存活会禁止宪章保留的网络跳后果所有转移都是可审计的派生图边——这正是这个域何时、从谁那里得到这项权力可查询的原因charter identity审计排序见 ADR-K7序列化干净消息指名槽与掩码而非地址REQ-ABI-5证据REQ-CAP-2。五、ADR-K4撤销Revocation上下文宪章§7要求撤销外部原子、内部可抢占自引用撤销不可表示且只在终态报告完成。机制必须做到这一点同时避开 seL4 文档化的病理中途撤销自己的权力会留下部分状态。决策撤销有两条路径均来自 ADR-K21. 批量失效对象或域死亡递增对象代引用旧代的每个能力在下次使用时立即失效O(1)。对象的池槽随后由增量清扫回收在抢占点下运行seL4 僵尸纪律期间对象处于显式dying状态——不可调用、不可被观察为存活、也尚未报告完成。2. 范围撤销撤销子委托、保住对象从指名能力出发遍历派生子树增量且可抢占地使每个条目失效对象与无关委托保持完整。两条路径共同点完成以终态为门死亡记录ADR-K5或 revoke-complete 返回只在清扫结束后发出自引用不可表示拆除一个域的权力的唯一来源是测量引导计划charter §7且它永不是该域自身表中的能力——域无法持有、因此也无法撤销用于销毁它自己的权力。被否决的替代方案方案否决理由(a) 完全同步原子撤销不可抢占被否决撤销大树是无限工作量会阻塞单 hart违反调度器的有界工作规则ADR-K6(b) 延迟/惰性回收先标记后收集对安全相关情形被否决重新打开威胁模型所关闭的陈旧引用窗口对比 IOTLB 惰性失效类别威胁模型 §6代递增使失效即时即使回收是增量的(c) 像 seL4 文档那样把自引用边界情形留给用户层构造回避被否决宪章的标准是在内核中使它们不可表示而不是警告用户空间后果失效即时无陈旧权力窗口回收有界且可抢占不对 hart 造成 DoS部分状态永不可观察REQ-FAULT-1自撤销不可能发生REQ-FAULT-3代递增/派生遍历的拆分正是 ADR-K2 混合机制兑现收益之处证据REQ-FAULT-1、REQ-FAULT-2、REQ-FAULT-3。六、ADR-K5故障端点Fault endpoints上下文宪章§7要求每个域终止产生恰好一条死亡记录投递给监督者supervisor投递槽在域创建时预留若监督者已死则重亲到看门狗。威胁模型标记的开放子问题故障域应该阻塞seL4 同步会合无缓冲可溢出还是排队Erlang 异步但我们负担不起无界邮箱决策每个域有一个故障端点内核对象。其监督者持有对该端点的接收能力由测量引导计划或显式监督授权建立绝不自持——见 ADR-K4。死亡投递是异步进入单个预留槽域创建时从恢复池铸一枚死亡记录槽绑定到故障端点因此投递永不分配、永不因容量不足失败charter §6、§7。这是同步 vs 异步问题的预留槽解决方案取异步模型的非阻塞属性垂死域不等活着的监督者却没有无界邮箱——因为邮箱恰好一个槽而且它已经存在。若记录到达时监督者已死记录连同监督者自己的死亡记录沿监督链向上重亲终止于看门狗看门狗由引导计划保证存活。被否决的替代方案方案否决理由(a) 同步会合seL4 故障处理器模型被否决死域已无物可阻塞且把拆除的活性耦合到监督者的活性(b) 无界队列Erlang monitor 模型被否决ring 0 不允许无界分配charter §2(c) 在故障域内联处理故障信号处理器风格被否决这是契约排除的 POSIX 信号模型且域不能被信任来处理自身故障后果恰好一次投递是结构性的一个槽、铸一次、消费一次REQ-FAULT-4、REQ-FAULT-5拆除活性独立于监督者活性看门狗是保证的终端监督者——这正是引导计划必须预留它的原因证据REQ-FAULT-4、REQ-FAULT-5、REQ-MEM-3恢复容量预留全局耗尽下拆除死亡报告监督者重启仍能完成。七、ADR-K6调度Scheduling上下文宪章要求抢占式调度、有界工作、显式每域预算首台机器单 CPU范围 §6.2。Realm 程序已把客户工作量按燃料fuel计量而预留容量规则charter §6意味着 CPU 与内存一样必须是可问责资源。决策CPU 时间是一种能力调度上下文对象周期 预算域必须持有它才能运行——形态由 seL4 的 MCS 内核验证。调度器是单 hart、抢占式、按优先级排序并强制预算域在其调度上下文有预算时运行预算耗尽将其抢占并引发其监督者可观察的有界超时条件可能长时间运行的内核操作撤销清扫ADR-K4正是预算所约束的可抢占工作——同一批抢占点同时服务调度与撤销预留恢复域与看门狗域持有的调度上下文保证它们在争用下仍获得 CPU镜像预留内存池。被否决的替代方案方案否决理由(a) 无预算的固定优先级抢占经典 RTOS被否决无问责 CPU 资源高优先级域会饿死他人且委托时没有可衰减的能力(b) 公平分享 / CFS 风格被否决对首版内核不确定且策略过重宪章要求在强制层确定性(c) 协作式让出Realm 当前的 slice 间模型对内核对被否决无法约束永不让出的恶意域威胁模型要求Realm 的协作模型在域内没问题内核在域间必须抢占后果CPU 与其他权力完全一样可委托、可衰减——子调度上下文是更短预算绝不是更长宪章的递归衰减原则预算耗尽是有界、可观察事件对应 MCS 超时异常设计现在单 hartSMP 是本 ADR 的 scope-M7 变更证据REQ-MEM-3为恢复预留 CPU、REQ-FAULT-6无限循环 → 有界拆除。八、ADR-K7审计排序Audit ordering上下文宪章§3、§7要求 ring 0 锚定一个序列或根哈希且永不解释记录现有 Astrid 审计链是用户空间构建的BLAKE3 密封、ed25519 签名链。待决策的是ring 0 提供什么排序保证密码链放在哪里。决策ring 0 对可审计的跨域事件能力派生、域生命周期、故障记录盖上单调全序——通过单个内核持有的序列计数器并通过维护**运行中的根running root**锚定完整性每个盖章事件推进一个哈希累加器其当前值 ring 0 会证明attest但永不解析。密码链本身在用户空间构建由审计系统宿主域威胁模型中的 T3读取有序事件流用 BLAKE3 密封每条目哈希前一条用 ed25519 签名——与现有 Astrid 审计设计完全不变。职责划分ring 0 保证顺序与无缺口每个序列号都被记账用户空间保证防篡改与真实性。二者组合验证者对照 ring-0 证明的根检查用户空间链因此被攻破的审计域不能静默丢弃或重排事件而不使根发散。仓库佐证现有用户空间审计链实现在 crates/astrid-audit 中。其 README 说明每条AuditEntry含动作/授权证明/结果、链接前一条目的 BLAKE3previous_hash创世条目使用ContentHash::zero()、签名该条目的运行时 ed25519 公钥与签名验证按会话检查三条不变量有效创世、有效签名、链接不断每条失败是类型化ChainIssue。具体字段在 src/entry.rs 中previous_hash: ContentHash、runtime_key: PublicKey、signature: Signature。链的密封序号与prior_receipt_hash的 BLAKE3 校验在 src/storage/prune_chain.rs 中可见。这正是 ADR-K7 ring 0 锚定、用户空间建链分工下用户空间侧已有工程基础。被否决的替代方案方案否决理由(a) 全审计链放在 ring 0内核做 BLAKE3 ed25519被否决把记录解释与密码策略放进 ring 0违反契约并膨胀 TCB(b) 排序完全交给用户空间被否决纯用户空间顺序无法在审计域被攻破时证明无缺口内核必须持有计数器与根链在 T3 沦陷下才可信(c) 每域独立序列、无全局顺序被否决跨域因果谁在何时授予谁什么需要全序可读性与委托审计都依赖它后果ring 0 的审计表面是一个计数器 一个哈希累加器——TCB 极小无记录解析charter §2现有用户空间链整体复用系统何时从谁那里学到 X与证明审计日志无缺口都可核查——这是内核事实与用户空间推理者/表述者的接缝有序、有根的事件流正是后来的推理者当作事实读取的东西证据REQ-LEG-1单一事实来源以及现有审计测试承载的审计链符合性。九、跨切面后果一条脊柱三个机制七项决策共享一条脊柱机制出现位置承载的属性派生图derivation graphADR-K2/K3能力完整性、范围撤销、审计来源查询代计数器generation counterADR-K2/K4O(1) 批量失效、即时失效预留池reserved poolADR-K1/K5/K6故障投递永不因容量失败、恢复/看门狗 CPU 与内存保证这是刻意的少量机制承载大量属性比一个属性一个机制更易验证、更易模糊测试。v0 ABI 草图下一工作计划项恰好只暴露这些域、能力表槽、调度上下文、故障端点、审计有序事件表面——除此之外不暴露任何需要路径、字符串主体或环境式句柄的东西对应宪章 §2 的字符串即权力禁令与REQ-CAP-3ABI 表面审查 编译期检查无任何 syscall 接受路径/URI 参数。与证据矩阵的映射速查矩阵docs/astrid-kernel-evidence-matrix.md规定属性未到测试失败即证明丢失之前不算持有并区分host、qemu、fuzz、build证据种类与 M1–M6 门槛。七项 ADR 直接引用的关键行能力与句柄完整性REQ-CAP-1伪造索引被拒qemu/M2、REQ-CAP-2加宽权限被拒qemu/M2、REQ-CAP-3无字符串主体build/M1、REQ-CAP-4清单声明不是权力qemu/M3内存与池纪律REQ-MEM-1定长槽、不可碎片化饿死hostqemu/M2、REQ-MEM-2每次铸币可失败可归因qemu/M2、REQ-MEM-3恢复容量预留qemu/M2、REQ-MEM-4W^Xqemu/M2撤销与故障语义REQ-FAULT-1外部原子、REQ-FAULT-2撤销完备、REQ-FAULT-3自引用撤销不可表示、REQ-FAULT-4恰好一条死亡记录、REQ-FAULT-5投递不因容量失败、REQ-FAULT-6组件陷阱留在 Wasmtime 内qemu/M3ABI 与解析器边界REQ-ABI-1全操作全函数、REQ-ABI-2边界处恰好一次复制校验、REQ-ABI-3解析器抗对抗输入fuzz、REQ-ABI-4无无界长度消息host/M1、REQ-ABI-5序列化下语义保持host/M2可读性与信道REQ-LEG-1内核状态单一事实来源无镜像事实库、REQ-LEG-2每关系能力门控、仅域可见、REQ-LEG-3时序相关关系限流与量化。十、结语为什么被否决的方案与被选择的方案同等重要从表面看七项 ADR 回答了域长什么样、能力怎么表示、句柄怎么转移、怎么撤销、故障怎么投递、CPU 怎么调度、审计怎么排序七个问题。但这份文档的深层价值在于记录约束如何参与决策契约covenant先行POSIX 进程形态、信号处理器式故障处理、ring 0 内建密码链——都不是因为难而被否决而是因为宪章 §2 永久排除了它们威胁模型参与否决惰性回收被否决是因为它重开威胁模型 §6 关闭的陈旧引用窗口协作调度被否决是因为它无法约束永不让出的恶意域机制复用优先代递增与派生遍历的混合ADR-K2/K4、预留槽同时解决投递容量与调度预算ADR-K5/K6、一个序列计数器加哈希累加器完成审计排序ADR-K7——少量机制承载多属性是这份决策日志贯穿始终的主线每条决策都锚定证据从REQ-CAP-1到REQ-LEG-1每个后果都有对应的可执行检查、证据种类与里程碑门槛保证这些架构选择不只是文档中的漂亮段落而是可被测试证伪的工程承诺。对于想深入代码的读者可从 crates/astrid-auditADR-K7 的用户空间链侧与 crates/astrid-cryptoBLAKE3 哈希与 ed25519 签名原语继续追踪而内核本身的骨架与 ABI 草图则在工作计划中列为后续里程碑其证据逐项挂在 证据矩阵 上等待兑现。赞分享【免费下载链接】astridAstrid is a portable, capability-secure operating system for composable software.项目地址https://gitcode.com/gh_mirrors/astrid2/astrid点击查看免费下载相关推荐ScrollingPagerIndicator打造Instagram风格的轻量级分页指示器完全指南ScrollingPagerIndicator打造Instagram风格的轻量级分页指示器完全指南 ScrollingPagerIndicator是一款受In用架构决策记录ADR保存设计系统的决策历史Carbon Design System 的实践用架构决策记录ADR保存设计系统的决策历史Carbon Design System 的实践 本文基于 docs/decisions/0001 record前端UI组件设计系统Authelia 配置架构决策记录 ADR2 深度解读环境变量、Secrets 与模板化配置的设计取舍Authelia 配置架构决策记录 ADR2 深度解读环境变量、Secrets 与模板化配置的设计取舍 本文以 Authelia 官方架构决策记录 ADR2:后端认证鉴权单点登录身份认证应用安全上一篇CANN元数据定义创建函数下一篇CANN ops-math ConcatDV2算子创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考