张倩颖 博士
讲师/硕士生导师
首都师范大学，信息工程学院
地址：北京市海淀区西三环北路56号219办公室
邮编：100048
Email：qyzhang@cnu.edu.cn
基本信息
张倩颖，博士，讲师/硕士生导师，2015年毕业于中国科学院软件研究所，获得计算机科学与技术工学博士学位，同年加入首都师范大学信息工程学院。
研究领域为高可信的安全嵌入式操作系统，研究方向包括基于硬件安全架构的嵌入式操作系统构建技术，以及嵌入式操作系统及安全敏感代码正确性、安全性、可靠性等属性的形式化分析方法。研究成果包括在CCS、RAID、Science Bulletin等国际顶级学术会议和国际期刊发表论文30余篇，获得国家授权发明专利5项，国家密码行业标准1项。目前主持国家自然科学基金1项，负责国家重点研发计划子课题1项，主持北京市教委项目1项。现为CCF形式化方法专业委员会委员，SCN、IJNS等国际期刊审稿专家。
研究兴趣
嵌入式操作系统、信息系统安全、形式化验证技术。
教育经历
2008.09 – 2014.12，中国科学院软件研究所，信息安全国家重点实验室，工学博士
2004.09 – 2008.06，华中科技大学，计算机科学与技术学院，工学学士
科研项目
1、[主持]国家自然科学基金青年项目，基于可信执行环境的机器人实时操作系统架构及形式化验证研究，2017/01-2019/12
2、[负责]国家重点研发计划“智能机器人”专项项目子课题，机器人操作系统及开发环境研究与应用验证，2018/01-2020/12
3、[主持]北京市教委科技计划一般项目，基于TrustZone技术的嵌入式双操作系统架构研究，2019/01-2021/12
4、[参与]国家密码管理局密码检测标准项目，可信计算 可信密码模块符合性检测规范，2018/07-2019/06
5、[参与]国家自然科学基金重点项目，可信计算环境测评理论和技术研究，2012/01-2015/12
6、[主持]北京高等学校高水平人才交叉培养“实培计划”项目，Linux安全管理系统界面开发，2019/06-2020/05
7、[主持]北京高等学校高水平人才交叉培养“实培计划”项目，基于2D视频重建3D人体运动姿态及识别技术研究，2019/06-2020/05
8、[主持]北京高等学校高水平人才交叉培养“实培计划”项目，嵌入式系统安全管理程序开发，2018/06-2019/05
9、[主持]北京高等学校高水平人才交叉培养“实培计划”项目，基于二维图片/视频的三维人体体型建模及识别技术研究，2017/06-2018/05
10、[主持]北京高等学校高水平人才交叉培养“实培计划”项目，基于机器学习的人头发三维模型重建技术研究，2017/06-2018/05
代表论文
[1]Shijun Zhao, Qianying Zhang*, Qin Yu, Wei Feng, Dengguo Feng. SecTEE: A Software-based Approach to Secure Enclave Architecture Using TEE. In Proceedings of the 26th ACM Conference on Computer and Communications Security (CCS), 2019 (CCF-A)
[2]Shijun Zhao, Qianying Zhang*, Yu Qin, Wei Feng, Zhining Lv, Dengguo Feng. Minimal kernel: An operating system architecture for TEE to resist board level physical attacks. In Proceedings of the 22nd International Symposium on Research in Attacks, Intrusions and Defenses (RAID), 2019 (CCF-B)
[3]Dongxu Ji, Qianying Zhang*, Shijun Zhao, Zhiping Shi, Yong Guan. MicroTEE：Designing TEE OS based on the microkernel architecture. In Proceedings of the 18th IEEE International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom), 2019 (CCF-C, Best Trust Track Paper Award)
[4]Meiyu Zhang, Qianying Zhang*, Shijun Zhao, Zhiping Shi, Yong Guan. SoftME: A software-based memory protection approach for TEE system to resist physical attacks. Security and Communication Networks, 2019 (CCF-C)
[5]Qianying Zhang, Zhiping Shi. A new way to prevent UKS attacks using hardware security chips. International Journal of Network Security, 2017,19(5):823-831
[6]Qianying Zhang, Shijun Zhao, Yu Qin, Dengguo Feng. Formal analysis of TPM2.0 key management APIs. Chinese Science Bulletin, 2014,59(32):4210-4224 (SCI)
[7]Qianying Zhang, Shijun Zhao, Li Xi, Wei Feng, Dengguo Feng. Mdaak: A flexible and efficient framework for direct anonymous attestation on mobile devices. In Proceedings of the 10th International Conference on Information and Communications Security (ICICS), 2014:31-48 (CCF-C)
[8]Qianying Zhang, Shijun Zhao, Yu Qin, Dengguo Feng. Improving the security of the HMQV protocol using tamper-proof hardware. In Proceedings of the 10th International Conference on Security and Privacy in Communication Networks (SecureComm), 2014:343-361 (CCF-C)
[9]张美玉, 张倩颖*, 孟子琪, 施智平, 关永. 实时嵌入式双操作系统架构研究综述. 电子学报, 2018,46(11):2787-2796
[10]张倩颖, 冯登国, 赵世军. TCM密钥迁移协议设计及形式化分析. 软件学报, 2015,(09):2396-2417
[11]张倩颖, 冯登国, 赵世军. 基于安全芯片的平台身份证明方案研究. 通信学报, 2014,35(8):95-106
[12]张倩颖, 赵世军, 冯伟, 秦宇, 冯登国. 跨平台的可信执行环境模块方案研究. 通信学报, 2014,35(Z2):72-85
授权专利
1、施智平，关永，吴爱轩，李黎明，李晓娟，王瑞，邵振洲，张倩颖，吴敏华，一种机械臂运动学形式化分析方法，CN1.X
2、赵世军，初晓博，张倩颖，秦宇，冯伟，一种保护终端配置隐私的可信网络接入方法及系统，CN 7.6
3、冯登国，冯伟，秦宇，初晓博，张倩颖，奚瓅，杨波，一种基于移动设备的可信模块及其可信服务方法，CN7.5
4、冯登国，秦宇，初晓博，张倩颖，冯伟，基于椭圆曲线和双线性对密码体制的直接匿名证明方法，CN0.X
5、冯登国，张立武，汪丹，李昊，张倩颖，一种基于平台身份的信任服务连接方法与信任服务系统，CN8.6
行业标准
国家密码行业标准，《可信计算 可信密码模块符合性测试规范》。
主讲课程
本科生课程：编译原理、计算机应用、计算机实践1；
研究生课程：形式化验证。
获奖情况
2019年，北京市高等教育学会计算机教学精彩片段交流一等奖；
2017年，北京市科学技术二等奖，机器人多核异构实时嵌入式操作系统研发、验证及应用；
2017年，首都师范大学信息工程学院青年教师基本功大赛二等奖。
研究生培养
研究内容：
针对移动互联网和物联网等热点研究领域的关键安全问题，重点研究面向智能终端及嵌入式设备的安全操作系统构建技术，包括：
基于ARM TrustZone技术的安全操作系统构建技术研究；
基于定理证明的嵌入式操作系统形式化验证技术研究；
安全敏感代码可靠性的形式化分析方法研究。
从而以高可信密码算法实现为支撑，操作系统设计、实现、形式化验证为技术路线，为智能终端及物联网设备构建高安全、高可信的操作系统。
招生要求及培养方向：
(1)嵌入式操作系统
要求喜爱程序设计，具有一定的操作系统和C语言程序开发基础，今后主要从事基于ARM TrustZone技术的安全操作系统构建技术研究。
(2)形式化验证
要求喜爱逻辑推理，具有一定的操作系统和离散数学基础，今后主要从事基于定理证明的嵌入式操作系统形式化验证技术研究、安全敏感代码可靠性的形式化分析方法研究。
欢迎有志于高安全、高可信的操作系统研究的同学来攻读硕士研究生！