杨璧丞

硕士生

bichengyang@sjtu.edu.cn

个人简介

  • 杨璧丞,硕士生二年级,上海交通大学并行与分布式系统研究所。在夏虞斌副教授的指导下,当前主要研究方向为TEE系统和系统软件的形式化验证。

学术经历

  • 2019.09 - 至今,上海交通大学软件学院,硕士生,导师:夏虞斌

研究方向

使用形式化验证的方法来保证系统软件的正确性。

研究项目

  • Penglai:蓬莱是一个基于RISC-V平台研发的可信执行环境软硬件系统

    http://penglai-enclave.systems/

  • Pangolin:基于模型检验与符号执行的TEE系统形式化验证框架

    软硬件协同是TEE系统的发展趋势,于是对其软件TCB部分进行形式化验证就十分自然与必要。Pangolin利用模型检验和符号执行,对TEE系统进行形式化验证。

助教工作

  • 2020.09 - 2021.01 上海交通大学 软件学院 计算机系统原理(研究生)

获奖情况

  • 2020.10 华为奖学金