浙江大学 赵永望 教授
报告生成时间：2026年8月25日
个人主页：赵永望
所属团队：浙江大学网络空间安全学院 / 区块链与数据安全全国重点实验室
一、学者基本信息
| 字段 | 内容 |
|---|---|
| 姓名 | 赵永望（Yongwang Zhao） |
| 出生年份 | （待核实） |
| 职称 | 教授（Full Professor）、博士生导师 |
| 所属单位 | 浙江大学计算机科学与技术学院 / 网络空间安全学院 |
| 实验室职务 | 移动终端安全技术浙江省工程研究中心主任；浙江大学嘉兴研究院数字安全创新中心科研十二部（翔云团队）负责人；区块链与数据安全全国重点实验室研究骨干（具体职务待核实） |
| 学术头衔 | CCF杰出会员（2021年当选）；CCF形式化方法专委会、系统软件专委会、网络与系统安全专委会、抗恶劣计算专委会执行委员 |
| 国家级人才 | 工信部重大专项项目首席科学家 |
| 其他任职 | 浙江省天目山实验室第一届理事会理事；望安科技（浙江望安科技有限公司）创始人、实际控制人 |
| 邮箱 | zhaoyw AT zju.edu.cn |
| 研究方向 | 形式化方法（形式逻辑、形式化验证、并发理论、定理证明 Isabelle/HOL、程序验证）、操作系统与安全（OS形式化验证、微内核/分区/隔离内核、Linux内核、ARINC653）、编程语言与编译（函数式编程、程序语义、可信编译）、安全认证（CC、DO-178 B/C、ISO 26262、IEC 61508）、AI/LLM辅助的定理证明与验证 |
二、教育背景与职业履历
赵永望的早期教育与职业履历集中于北京航空航天大学计算机学院：其博士阶段在北航完成（导师及具体年份待核实，早期论文与马殿富教授团队联合署名，可推断其博士训练与北航软件工程研究所相关）。在北航期间，他从讲师/副教授起步，长期从事操作系统内核及安全、形式逻辑与验证、安全攸关系统与模型驱动方法研究，主讲《离散数学》《形式语言与自动机》《软件体系结构与中间件》《中间件技术》等课程，主持和参与国家自然基金课题、国家核高基重大专项等十余项。早期研究以Web服务、协同可视化与服务组合（SOA）为切入点，曾担任国际标准化组织 ISO/IEC JTC1 SOA研究组组长，起草4项ISO国际标准、12项国家标准。
其后，赵永望赴新加坡南洋理工大学（NTU）担任高级研究员，参与新加坡NRF重大项目等课题。2018年前后（具体加入时间待核实）加入浙江大学计算机科学与技术学院/网络空间安全学院，任教授、博士生导师，并逐步在浙大建立起国内操作系统形式化验证领域的代表性团队：2017年正式成为ARINC653国际操作系统标准委员会成员（中国首个成员，后被称为"国内唯一委员"）；2018年受邀成为国际信息技术安全评估标准（Common Criteria, CC）操作系统内核工作组成员；2021年当选CCF杰出会员；2022年其团队完成元心安全微内核操作系统V2.0的形式化建模与验证及EAL5+评估服务，助力元心OS获得当时国家级评测机构颁发的最高EAL安全级别软件评测证书；2023年承担小米自研TEE系统（MiTEE）的形式化验证与EAL5+高等级安全认证工作，成为小米澎湃OS的安全技术底座，其本人以"安全代言人"身份亮相2023年10月26日小米新品发布会。2023年获批国家自然科学基金叶企孙科学基金项目"泛在操作系统的形式化建模与评估验证方法研究"（联合申报）。2025年发起并组织中国"第一届定理证明竞赛"；2025年12月受邀担任IEEE PES电力系统通信与网络安全技术委员会（中国）开源软件技术分委会常务理事。其成果发表于 ACM TOPLAS、ACM TOSEM、IEEE TDSC、TACAS、CAV、FM、ISSRE、ICML、CCS、OOPSLA 等顶级期刊与会议，其中2020年TOPLAS论文与2024年OOPSLA 2025论文均为浙江大学首次以第一作者单位在该期刊/会议上发表。
三、学生培养情况
1. 赵健宏（浙江大学网络空间安全学院2022级博士生，博士导师直接指导）
赵健宏为赵永望直接指导的博士生，2022年与康锦辉一起由赵永望带队，联合数据通信科学技术研究所、中国农业银行组成"一颗红心"战队，参加"2022金融密码杯全国密码技术大赛"（中国人民银行与国家密码管理局指导、央行数字货币研究所与清华密码理论研究中心主办的国内最高规格金融行业密码大赛），凭借"面向金融应用场景的智能合约形式化验证技术与工具"斩获创新赛道一等奖。该工作结合金融领域实际需求，研发了基于形式语义、支持复杂规约的高安全、多合约语言形式化验证原型工具。此案例体现了赵永望将形式化验证方法应用于区块链与智能合约安全的育人方向（博士论文题目与后续去向待核实）。
2. 康锦辉（浙江大学网络空间安全学院2022级硕士生，硕士导师直接指导）
康锦辉为赵永望直接指导的2022级硕士生，与赵健宏同为"金融密码杯"一等奖战队核心成员，参与智能合约形式化验证技术与工具的研发（后续去向待核实）。
3. 翔云团队成员（团队培养）
赵永望领衔的翔云团队（依托浙江大学网安学院和浙江大学嘉兴研究院，2022年7月正式成立）汇聚了毕业于浙江大学、北京航空航天大学、厦门大学、杭州电子科技大学等重点高校的十多位博士/硕士和工程师，在操作系统、无人机研发等领域开展系统化人才培养。团队成果包括 FlyAir 系列高安全无人机（2022年12月FlyAir试飞成功、2023年8月FlyAir2.0试飞成功）、FlyCube高安全航空机载平台（2023年9月亮相）、Matrix653多核机载操作系统（与翼辉信息合作）。团队成员以团队培养为主要关系类型（个体名单待核实）。
4. 胡帅等论文合作学生（论文合作/博士导师直接指导）
赵永望团队在TOPLAS、OOPSLA等顶会顶刊上以第一作者单位发表论文的学生（如2021年TOPLAS论文、2024年OOPSLA 2025论文的第一作者，具体姓名待核实）属于其博士导师直接指导的谱系成员。
四、学术合作网络
4.1 实验室内部合作
在浙江大学内部，赵永望与网络空间安全学院/区块链与数据安全全国重点实验室的同事保持合作关系：2023年其叶企孙科学基金项目"泛在操作系统的形式化建模与评估验证方法研究"为联合申报，与实验室骨干（具体联合申报人待核实）协作。其形式化验证方向与网安学院重点发展方向深度绑定——学院层面已将形式化方法列为重点发展方向，赵永望团队是该方向的核心力量。与任奎（实验室常务副主任）、陈纯院士（实验室主任）所在的学院科研共同体存在制度性协作（具体合作论文待核实）。
4.2 跨机构合作
赵永望的跨机构合作网络极为丰富：与北京航空航天大学的长期渊源（其本人出自北航计算机学院，翔云团队部分成员亦毕业于北航，望安科技曾获"北航软件学院产教融合突出贡献奖"）；与中国电子技术标准化研究院联合主办嵌入式操作系统标准研讨会（2021年11月），并作为主要单位之一发起成立全国信标委操作系统标准工作组（2022年）；与浙江大学嘉兴研究院共建翔云团队；与元心信息科技集团（元心安全微内核操作系统EAL5+认证）、翼辉信息（Matrix653操作系统研发）、小米科技（MiTEE形式化验证与EAL5+认证、澎湃OS安全底座）、数据通信科学技术研究所与中国农业银行（金融密码杯智能合约验证）等开展深度产学研合作；与望安科技所服务的载人航天工程、中航工业、航天科技、航天科工、军事科学院、中国信科、中国移动、中科海微等机构形成产业应用网络；与首都师范大学信息工程学院（2025年学术报告）等高校有学术交流。
4.3 国际合作
赵永望的国际合作以国际标准化组织为枢纽：ARINC653国际操作系统标准委员会（成员来自波音、空客、洛克希德马丁、GE航空、霍尼韦尔、达索航空、泰雷兹、罗克韦尔柯林斯、风河WindRiver、绿山Green Hills、DDC-I、SYSGO等，委员会主席由波音与空客专家担任）——他2017年正式入会（中国首个成员），2018年在法国Thales总部参会时其IEEE TDSC论文被专题讨论、发现的6个安全漏洞获标准委员会确认并修改标准，2018年11月受邀访问法国空客总部，2019年参与研制的ARINC653新版标准正式发布。Common Criteria（CC）操作系统内核技术委员会（2018年受邀加入）。2014年曾组织访问德国、奥地利、荷兰、卢森堡的欧洲大学（含慕尼黑工业大学、维也纳工业大学等），签署安全关键实时系统与形式化方法领域的合作备忘录。其研究成果被法国开源操作系统内核POK引为重要参考文献（POK后被开发为商用JetOS并应用于俄罗斯民航客机），并在2025年ICFEM国际会议作大会特邀报告（TRust2: Rust语言在Isabelle/HOL中的形式化验证工具链）。此外，其团队发起的TPChina定理证明开放社区（2020年）和Isabelle/Cloud定理证明云平台（2023年发布）亦具国际开放生态属性。
五、业界合作关系深度分析
5.1 产业合作
赵永望的产业合作呈现"高安全认证服务"的鲜明特色：为元心科技的元心安全微内核操作系统V2.0提供形式化建模验证与EAL5+评估服务，获国内首张国家级最高安全级别（EAL5+）软件评测证书（2022年）；为小米自研TEE操作系统（MiTEE）提供形式化验证与EAL5+高等级安全认证（2023年），成为小米澎湃OS"全域安全"的技术底座，并以"安全代言人"身份亮相小米新品发布会；指导翼辉信息研发符合ARINC653标准的Matrix653机载操作系统并合作研发高安全认证版本；与中国电子技术标准化研究院共同推进嵌入式操作系统国家标准体系建设。其产业足迹覆盖航空航天（波音、空客认可）、国防军工（中航工业、航天科技/科工、军事科学院）、通信（中国移动及某大型通信企业）、消费电子（小米）等国家关键行业。
5.2 创业孵化与开源生态
赵永望于2019年6月创立浙江望安科技有限公司，作为创始人、实际控制人（直接持股约18.46%-20%，最终受益股份72.94%），公司定位为网络信息安全产品及服务提供商，聚焦形式化验证解决方案、产品安全认证服务与"望安穹道"原生安全平台。2024年5月获深创投集团千万级天使轮融资，2026年入选《2026浙大系未来独角兽企业榜单》，公司先后中标某大型央企集团和某大型通信企业操作系统高等级安全合规项目。在开源生态方面，他深耕开源社区：担任IEEE PES开源软件技术委员会分委会常务理事（2025年），其研究被开源内核POK引用，发起TPChina定理证明开放社区，发布Isabelle/Cloud云平台，并在2023年第一届开放原子开源基金会OpenHarmony技术峰会上作"操作系统形式验证与安全认证"主题报告。团队编写的《PiCore形式化方法与实践》《函数式程序设计与证明》等开源书籍亦是其知识传播生态的一部分。
六、重要奖项与学术兼职
| 类别 | 名称 | 年份 | 说明 |
|---|---|---|---|
| 科技奖励 | 山东省科技进步一等奖 | 2017 | 省部级科技进步一等奖 |
| 科技奖励 | 中国电子学会电子信息科技一等奖 | 2011 | 省部级科技奖励 |
| 人才/荣誉 | CCF杰出会员 | 2021 | 中国计算机学会个人最高级别会员荣誉之一 |
| 竞赛指导 | "2022金融密码杯全国密码技术大赛"创新赛道一等奖 | 2022 | 指导赵健宏、康锦辉等组成的"一颗红心"战队（国内最高规格金融密码赛事） |
| 论文荣誉 | ACM FAC期刊2023年度Featured Article | 2024 | 团队论文获ACM Formal Aspects of Computing年度精选 |
| 科研项目 | 国家自然科学基金叶企孙科学基金项目 | 2023 | "泛在操作系统的形式化建模与评估验证方法研究"（联合申报） |
| 里程碑成果 | 国内首张TEE OS最高安全等级EAL5+证书 | 2023 | 小米MiTEE经形式化验证获CCRC颁发的国内首张EAL5+证书；2022年元心OS EAL5+为国家级机构首张软件类EAL5+证书 |
| 兼职 | 期限 |
|---|---|
| ARINC653国际操作系统标准委员会委员（国内唯一/首个成员） | 2017年至今 |
| 国际信息技术安全评估标准（CC）操作系统内核技术委员会委员 | 2018年至今 |
| 国际标准化组织 ISO/IEC JTC1 SOA研究组组长 | （曾任，期限待核实） |
| 移动终端安全技术浙江省工程研究中心主任 | （待核实起止时间） |
| 浙江省天目山实验室第一届理事会理事 | 2023年起 |
| IEEE PES（中国）开源软件技术分委会常务理事 | 2025年12月起 |
| IEEE Access期刊副主编 | （期限待核实） |
| 国家信标委分委会委员、全国信标委操作系统标准工作组主要发起成员 | 2022年起（具体期限待核实） |
七、Connection圈层总结
第一圈层（核心圈层）为赵永望的直接学术谱系与浙大团队：北航时期的导师与合作者马殿富教授（Dianfu Ma，北航计算机学院，其早期论文的资深合作者与可能的博士导师）及北航软件工程团队构成其学术血统；直接指导的博士生赵健宏、硕士生康锦辉（金融密码杯一等奖）、TOPLAS/OOPSLA论文的第一作者学生们，以及翔云团队（依托浙大嘉兴研究院）的十多位博士/硕士工程师构成其人才辐射网络。其本人创立的望安科技则是核心圈层的产业延伸。
第二圈层为浙大院内与省内平台：浙江大学网络空间安全学院与区块链与数据安全全国重点实验室（主任陈纯院士、常务副主任任奎）为其制度性依托；移动终端安全技术浙江省工程研究中心（任主任）、浙江省天目山实验室（理事会理事）、浙江大学嘉兴研究院（数字安全创新中心）构成其省内科研平台网络。
第三圈层为国内跨机构与产业合作网络：北航（学术渊源与产教融合）、中国电子技术标准化研究院与全国信标委（标准体系）、元心科技、翼辉信息、小米（操作系统安全认证）、数据通信科学技术研究所与中国农业银行（金融密码与智能合约验证）、载人航天工程及军工央企集团（高安全合规），以及首都师范大学等学术交流院校。
第四圈层为国际合作与标准化圈层：ARINC653标准委员会（波音、空客、霍尼韦尔、GE航空、泰雷兹、风河、绿山、SYSGO等）、Common Criteria操作系统内核工作组、欧洲高校合作网络（慕尼黑工业大学、维也纳工业大学等）、法国POK/JetOS开源社区影响，以及ICFEM等国际会议的特邀报告舞台。总体而言，赵永望的学术网络呈现出"北航软件工程训练—国际标准化舞台—浙大网安全国重点实验室—创业孵化（望安科技）"的四级跃迁结构，其以操作系统形式化验证为轴心，向国际标准制定、高安全认证服务、AI赋能定理证明和开源生态四个方向辐射，是国内罕有的同时贯通国际标准组织、国家测评机构、头部企业与学术顶会顶刊的学者型创业者。