Isabelle安全协议端到端验证博士

项目概览

埃克塞特大学计算机科学系提供“使用Isabelle开展安全协议端到端验证”的全日制Computer Science博士，编号6011，地点Streatham校区Kathleen Booth Building，2027年9月入学。申请截止2026年12月8日中午12:00 GMT，即北京时间20:00。包括中国在内的合格国际申请人可竞争最长3.5年DLA资助；获奖者全额学费含学校豁免国际差额，£21,805仅为2026/27津贴参考并随标准调整，£5,000研究培训费为3.5年全期合计。国际名额最多占队列30%，签证、IHS及搬迁自理。

项目详情

现代安全系统往往依赖复杂软件，把程序翻译成能够自动检查的表示。要信任这些系统，单独验证底层安全协议还不够，还必须知道被检查的表示是否忠实反映原本打算运行的程序。这个博士希望研究如何通过定理证明建立从程序到安全协议的端到端保证。研究目标是让多个层面的正确性联系起来，而不是把某次工具检查成功直接当作整个系统已经安全。

工作重点是验证程序与安全协议所用表示之间的翻译，主要形式化环境为Isabelle／HOL。零知识证明系统是重要应用方向之一，其中包括STARK类协议。中央问题在于怎样连接程序、编译过程及密码协议，使正确性和安全保证能够组合、重用。零知识证明是研究应用范围，不表示该博士只研究某个区块链产品，也不代表招聘已经公布具体协议实现或完成的系统证明。

项目横跨形式化方法、程序设计语言、网络安全与密码学，方向可结合学生兴趣调整。博士将发展并验证语义模型及编译技术，在Isabelle／HOL中说明生成的表示确实对应源程序行为。较长期目标，是进一步把这些结果同底层验证协议的机械化安全论证联系起来。因此，程序语义、翻译正确性与协议安全是相互连接但仍需分别建立证据的层次，不能省略中间环节。

介绍强调“发展并验证”模型及编译方法，属于拟开展的研究工作；未声称现在已经有覆盖全部程序或全部密码协议的完整端到端证明。它也没有公布唯一编译器、源语言、程序规模、固定性能指标或指定发表数量。具体的首阶段形式化对象、已有代码库及可重用定理，需另向团队了解，不能根据Isabelle或STARK名称自行补写。

导师团队具有Isabelle、形式化方法、智能合约验证及安全协议验证经验。当前具名项目列主导师Diego Marmsoler（d.marmsoler@exeter.ac.uk）及Achim Brucker（A.Brucker@exeter.ac.uk）。团队范围说明学术交叉，但未承诺每项专业都由同一名导师日常指导，也未公布指导比例、会面频率或专属计算资源。

申请要点

项目适合对形式化验证、程序语言、网络安全、密码学、编译器或定理证明有兴趣者；已有Isabelle或零知识证明经验有帮助，非必需。项目额外门槛写N/A，仍须满足一般相关科学技术领域First/2:1等值要求，2:2可结合硕士或显著相关非学术经历考虑。中国PGR通常看三年制硕士及毕业、学位材料，个人等值由招生审核；计算机英语Profile A为IELTS Academic总6.0、各6.0或认可替代。经具名PDF的APPLY HERE入口申请，最多三个项目分别提交，个人陈述写偏好；交项目陈述、CV、成绩单、两封推荐信和适用英语证明，全部材料用英文，学历非英文须认证翻译。推荐信最迟于2027年1月8日送达pgrapplicants@exeter.ac.uk，使用机构邮箱或合规机构抬头签字件。

12月8日中午是本轮申请截止，1月8日是推荐信最迟送达日期，两者不同。£21,805属于2026/27生活津贴参考，不是雇佣工资、未来固定金额或个人自动获奖保证。

需要进一步确认

仍需落实个人学历及英语等值、日常指导分工、首个源程序与表示、现有形式化库及编译与协议安全的衔接、预期贡献边界和证明困难时的阶段成果。2027实际个人津贴、支持结束日和可能的无资助写作期也应确认。

已核申请与资助依据：院系DLA轮次、2027国际资助条款、具名项目PDF。

博士项目深度研究报告：用 Isabelle 建立安全协议的端到端验证链

项目判断

研究主线清楚，重点核实课题边界与个人资格。 这个项目追问的是：安全协议检查的表示，是否真的对应原始程序？博士工作将用 Isabelle/HOL 连接程序语义、经验证的编译转换与协议安全论证，零知识证明及 STARK 类协议是重要应用场景。它适合从形式化方法、程序语言或密码学切入研究；已有 Isabelle 或零知识证明经验有帮助，但官网明确不作必备条件。导师为 Diego Marmsoler 与 Achim Brucker，地点是埃克塞特大学 Streatham 校区。准备申请前，先与团队确认初期研究的语言、转换环节和协议范围。具名项目说明

2027 年 9 月入学的 EPSRC DLA 竞争面向包括中国在内的国际申请人，资助最长 3.5 年。申请截止为 2026 年 12 月 8 日英国中午，即北京时间当日 20:00。 当前计算机轮次要求两封推荐信最迟于 2027 年 1 月 8 日 送达。资金是竞争结果，不是提交申请即可获得。学院项目页DLA 总规则

研究问题与博士工作

要补上的保证是什么

即使协议正确检查了某个数学表示，只要从原始程序到该表示的转换有误，检查通过也不能说明原始程序满足预期性质。项目要连接原始程序、编译得到的可检查表示以及验证协议的安全论证，使不同层次的正确性和安全保证能够组合、复用。重点是这条保证链是否成立。项目 PDF

招聘明确的工作包括：在 Isabelle/HOL 中建立并验证语义模型与编译技术；证明生成的表示忠实保留源程序行为；长期进一步连接底层验证协议的机械化安全论证。研究跨越形式化方法、程序语言、网络安全与密码学，可根据学生兴趣调整。零知识证明与 STARK 类协议是重要应用，但官网没有指定唯一协议实现、源语言或必须采用的密码构造。

讨论课题时，需要区分“程序如何执行的模型”“转换保留模型行为的定理”和“验证协议的密码学安全定理”。这些结论可能依赖不同假设，只有接口和假设吻合，才能组合成端到端保证。梳理各层保证与仍需信任的部分，是从公开目标推导出的潜在研究切口，并非导师已确定的工作包。

导师已有的 Solidity 源语言验证和 EVM 字节码语义提供相关基础，但源语言证明本身不等于目标程序行为正确，也不等于零知识协议已经安全。近期 EVM 论文仍报告未覆盖的操作与验证失败。因此，限定语言子集、模型范围和密码假设，会直接影响研究结论的可信度。Solidity 浅嵌入Isabelle/EVMSSCalc

学校、学科与培养

这是埃克塞特大学计算机科学博士，具体项目为全日制，位于 Streatham 校区 Kathleen Booth Building。DLA 计划对应 2027 年 9 月入学，最长资助 3.5 年；资助结束不代表任何延长写作期都继续发放生活津贴。埃克塞特是培养与授位大学，公开信息没有联合学位安排。项目地点与学位DLA 计划

学校中国页面报告 QS 2027 综合第 136 名；计算机博士项目页列出 Complete University Guide 2027 英国计算机科学第 17 名、Times/Sunday Times 2027 同学科第 20 名。综合排名和英国学科排名的范围不同，均不能视作这对导师或 Isabelle 研究小方向的排名。与课题更直接的条件，是系内安全与分布式系统团队持续开展交互式定理证明、语言安全和智能合约正确性研究。学校信息计算机培养项目相关研究团队

现行计算机博士进阶规则要求第 9 个月末前提交不超过 5,000 词的升级报告，六周内进行口试，整个升级过程须在第 12 个月内完成。后续第 20、30 个月有研究报告与小型口试，第 30 个月还须提交论文结构及完成时间表。应以入学时适用规则为准；同一手册邻近的数学课程学时要求，不能直接套用于本计算机项目。计算机升级规则后续进展考核

导师、团队与近期论文

PDF 指定主导师 Dr Diego Marmsoler，邮箱 d.marmsoler@exeter.ac.uk；另一导师为 Professor Achim Brucker，邮箱 A.Brucker@exeter.ac.uk。Marmsoler 研究 Isabelle、程序语义和区块链验证。个人页面写 senior lecturer，系内团队页写 lecturer，故此处采用不受职级更新影响的 Dr 称谓。Brucker 的主页列明网络安全讲席教授及软件保障与安全团队负责人；其 SAP 安全开发经历属于历史履历。Marmsoler 主页Brucker 主页

团队从源代码、二进制和抽象规范层面结合验证、静态分析与测试。计算机博士培养说明包含主副导师、关怀导师及定期会面，系内提供计算机与 GPU/HPC 使用条件。公开页面没有确认本项目专属算力、密码学共同指导人员、企业实习或导师当前带生负荷。团队方向培养支持

近期三项重要成果：

1. Isabelle/Solidity 浅嵌入，AFP，2026。 Marmsoler、Asad Ahmed 和 Brucker 建立存储模型、表达式与语句浅嵌入、定制命令及验证条件生成器。档案摘要报告单元测试和四个案例，说明降低证明复杂度的工具价值。这是形式化证明档案成果，与 2024 年会议论文相关，不能重复算成两项独立发现，更不等于 STARK 安全证明。本次阅读档案摘要、作者日期及会话目录。原始档案

2. Isabelle/EVM，FMBC 研讨会，2026。 Ashley Card 与 Marmsoler 提供含跨合约执行的可执行 Isabelle 语义，并导出 Haskell。完整评价段显示：实际运行的 2,669 个测试文件中，1,966 个通过，约 74%；703 个失败，其中至少 440 个与未实现的预编译合约有关，另有 124 个文件跳过。因此不能把摘要中的约 25,000 个测试写成“全部通过”。Keccak 在证明模型中采用抽象定义，执行时接入外部具体实现。这项成果提供编译验证的字节码目标，也明确显示覆盖和信任边界。本次阅读摘要、作者、引言、部分语义与代码生成段及评价，未审计完整证明与代码。原始论文

3. SSCalc 演绎验证，Science of Computer Programming 243，2025。 Marmsoler 与 Billy Thornton 机械化证明演算的可靠性，并以定理支持合约类型实例的不变量证明，通过 token 案例展示。它的贡献是减少直接从语义推理的负担，不能扩写成任意合约安全或零知识性质已获证明。本次实际阅读出版社索引中的摘要、亮点与书目信息，未核读完整方法。出版社记录

三项工作支持团队在语义与证明工具方面的连续积累，尚不能证明拟开展的端到端密码保证链已完成，也不意味着博士只能研究 Solidity/EVM。

资助、申请与生活成本

详细规则列出最长 3.5 年、随标准调整的生活津贴，引用 2026/27 年每年 £21,805，另含学费和整个 3.5 年合计 £5,000 的研究培训支持。2027/28 年实际津贴应再次确认。国际学费身份获奖者最多占队列 30%，这是队列上限，不是中国申请人的录取概率；成功获得国际名额者，由学校豁免海外与本土学费的差额。签证费、医疗附加费及搬迁费不在奖学金覆盖内。详细资助条款国际生规则

必须使用项目 PDF 中的申请入口，总规则明确其他路线不具备这项资助资格。计算机方向最多申请三个项目，每项分别提交，并在个人陈述写明优先项目。材料包括 CV、说明学术兴趣、研究经历及项目选择理由的个人陈述、成绩单、两封推荐信和英语证明；尚未毕业可按要求提供现阶段成绩，非英文文件需认证翻译。两封推荐信须最迟于 2027 年 1 月 8 日 送达 pgrapplicants@exeter.ac.uk，使用机构邮箱或合规机构抬头签字件；全部申请材料用英文。培养项目的一般六月、七月申请日期不能替代本轮 DLA 截止。可能先有技术面试，再参加计划于 2027 年 2 月 15—24 日进行的统一面试，结果预计三月起发出。学院申请要求申请路线

学校依据 2026 年 4 月当地支出估计，单人基本生活预算约 £1,300—£2,000/月。以 £21,805 除以十二，约为 £1,817/月，与该区间相比约结余 £517 至缺口 £183；尚未计入不覆盖的初期费用。这只是基准比较，不是储蓄承诺或 2027 年报价。住房、账单和个人生活方式影响很大，入境、押金与安置需另备现金。官方生活预算

资格与准备重点

官方学历要求： 相关科学、工程或技术领域英国一等或 2:1 本科及等同学历；2:2 可以结合硕士学历，或显著相关的非学术经历考虑。项目 PDF 的额外门槛写 N/A。中国学历说明： 研究型研究生一般要求完成国内三年制硕士，并取得毕业证和学位证；官网本科 75%/70% 对照表适用于授课型硕士，不能直接当作博士分数线。硕士成绩对照表也限定了页面所列院校档次，个体等效资格须由招生部门确认。英语： 计算机博士对应 Profile A，IELTS Academic 总分 6.0，且每项不低于 6.0。学历规则中国研究型学历说明英语 Profile A

官方优先经验： Isabelle 或零知识证明经验有帮助，均非必需。分析建议： 用简洁材料解释自己做过的语义模型、不变量或编译正确性论证，说明哪些假设仍需信任，并展示可复现的数学或软件研究。这些是准备建议，不是新增的强制文件。仅展示应用开发、却不愿处理逻辑定义和证明维护，较难说明与项目任务的关联。

职业能力主要指向形式化验证、可信编译和软件保障研究。英国政府 2026 年网络安全劳动力报告估计相关从业者约 145,900 人，核心岗位广告较 2024 年回升 7%，但从业规模增速仅 2%。这是英国整个网络安全市场背景，不能换算为定理证明岗位数量、本项目就业率或毕业薪资。专业研究作品比泛泛的“网络安全缺人”更有解释力。政府市场报告

下一步与待确认问题

申请前： 确认初期源语言、检查表示和协议对象；确认个人中国学历等值，并安排推荐信最迟1月8日送达；随后经 PDF 入口，在 12 月 8 日英国中午前提交具名项目申请。

面试时： 询问哪些语义和密码假设仍需信任，如何评价证明复用，博士贡献如何区别于已有库的扩展；确认专门密码学指导、会面频率和证明工具维护支持。

接受录取前： 取得实际津贴调整、完整海外学费豁免、支持结束日期和可能无资助写作期的书面条款；确认入学适用的注册升级规则及可负担住房。技术范围、指导容量和个人入学资格仍是需要落实的关键条件。

证据与来源

项目与资助

• Official Computer Science DLA award6011
• Named Isabelle project PDF
• DLA scheme overview
• DLA important information

学校与培养

• Computer Science doctoral programme
• English Profile A
• China qualification guidance
• CS first-year upgrade
• CS progress milestones

导师与研究

• Diego Marmsoler academic profile
• Achim Brucker academic profile
• Isabelle/Solidity shallow embedding AFP2026
• Isabelle/EVM FMBC2026
• SSCalc journal paper2025
• Official Secure and Distributed Systems group
• Software Assurance and Security team

成本与职业

• Local student budgeting April2026
• UK cyber labour market2026