Bin Fang

当前就职于华为中央软件部，形式化验证专家，从事系统安全研究、AI 安全研究。博士毕业于巴黎西岱大学 & 华东师范大学（中法联合培养 2014–2018），师从华东师大蒲戈光教授、法国Ahmed Bouajjani和Mihaela Sighireanu教授。研究兴趣包括功能安全 & 信息安全（safety & security）、系统安全、形式化验证、程序分析、AI 安全等。

Email GitHub Scholar
Bin Fang

项目经历

2025 - 至今

AI 辅助研发研究

探索形式化规约（Formal Spec）引导的 AI 辅助研发范式

2025 - 至今

AI 安全项目

探索 Agent 安全机制，包括动态权限管控、Agent 行为运行时安全等技术

2019 - 至今

鸿蒙内核/TEE 形式化验证 项目经理 · 架构师 · SE

探索大规模代码自动化形式化验证技术，开发形式化验证工具和程序分析平台，加固基础软件安全。部分技术发表于 CAV，成果上华为 HDC 发布会 KN

2018 - 2021

鸿蒙内核 EAL5+/6+ 信息安全认证 项目经理 · 安全工程师 · 形式化技术 SE

主导鸿蒙内核 CC EAL5+ 和 EAL6+ 信息安全认证形式化验证工程，开发形式化证明平台，通过欧洲认证机构评估。支持鸿蒙内核获得 CCEAL6+ 首个商用 OS 类产品认证，成果上手机发布会 KN

2019 - 2020

鸿蒙内核 ISO 26262 功能安全认证 项目经理 · Safety Manager · TUV 认证安全工程师

负责鸿蒙内核端到端功能安全认证，制定 ISO 26262 软件产品功能安全认证流程，完成 ASIL-D 认证

2013 - 2018

程序分析与 RTOS 形式化验证 核心研发

开发基于抽象解释的静态分析工具（heap-manipulating 程序、指针运算、内存安全）；参与 RTOS 形式化安全验证，与 B 方法发明人 Abrial（欧洲科学院院士）合作

工作经历

2024 - 至今

主任工程师 · 安全专家 · 技术经理

华为 · 上海

上海交通大学企业博导

2019 - 2022

高级工程师 · 项目PL&PM

华为 · 上海

交通-华为联培经理

2014

课程助教

华东师范大学 · 上海

研究生程序分析课程

2013.06 - 2013.09

研究实习生

上海高可信计算重点实验室 · 上海

教育背景

2014 - 2018

中法联合培养博士

巴黎西岱大学 & 华东师范大学 · 计算机科学 · 形式化验证

导师：蒲戈光教授、Ahmed Bouajjani 教授、Mihaela Sighireanu 教授

2013 - 2014

本科直博生

华东师范大学 · 软件工程理论与技术

2009 - 2013

学士

华东师范大学 · 软件工程

发表论文

  • 1.
    Enabling Semantic Evolutionary Analysis of Application via High-Precision Binary Diffing Bin Fang et al. Under Submission, 2026
  • 2.
    AgentVerify: Compositional Formal Verification of AI Agent Safety Properties via LTL Model Checking Bin Fang et al. Preprint, 2025
  • 3.
    Affine Loop Invariant Generation via Matrix Algebra Yucheng Ji, Hongfei Fu, Bin Fang, Haibo Chen The 34th International Conference on Computer Aided Verification (CAV), 2022
  • 4.
    Formal modelling of list based dynamic memory allocators Bin Fang, Mihaela Sighireanu, Geguang Pu, Wen Su, Jean-Raymond Abrial, Mengfei Yang, Lei Qiao SCIENCE CHINA Information Sciences, 2018
  • 5.
    A refinement hierarchy for free list memory allocators Bin Fang, Mihaela Sighireanu ACM SIGPLAN International Symposium on Memory Management (ISMM), 2017
  • 6.
    Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators Bin Fang, Mihaela Sighireanu International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2016
  • 7.
    Formal Development of a Real-Time Operating System Memory Manager Wen Su, Jean-Raymond Abrial, Geguang Pu, Bin Fang International Conference on Engineering of Complex Computer Systems (ICECCS), 2015
  • 8.
    Automated Coverage-Driven Test Data Generation Using Dynamic Symbolic Execution Ting Su, Siyuan Jiang, Geguang Pu, Bin Fang, Jifeng He, Jun Yan, Jianjun Zhao International Conference on Software Security and Reliability (SERE), 2014
  • 9.
    Runtime Verification by Convergent Formula Progression Yan Shen, Jianwen Li, Zheng Wang, Ting Su, Bin Fang, Geguang Pu, Wangwei Liu Asia-Pacific Software Engineering Conference (APSEC), 2014

荣誉奖项

China National Scholarship for International Doctorate

2014-2018 · France

Marktoberdorf Summer School Scholarship

2017 · Germany

MOVEP Summer School Scholarship

2016 · Italy