• 模型检查
• 系统分析与验证
• 计算机安全

招收硕士、博士

081202-计算机软件与理论
081203-计算机应用技术
081220-信息安全

系统分析与验证

2009-12--2013-04   巴黎狄德罗大学（巴黎七大）   博士
2007-03--2009-06   华东师范大学   硕士
2002-09--2006-06   宁波大学   学士

研究生

博士

2016-01~2016-07,华东师范大学, 副研究员
2013-08~2015-12,华东师范大学, 讲师

2016-03-01-今,中国计算机学会, 形式化方法专业组委员

信息安全研究方法
嵌入式系统开发实践

   

[1] 宋富, 陈光科, 赵哲. 基于语音声学特征压缩的语音对抗样本防御方法及应用. CN: CN114242083A, 2022-03-25.
[2] 宋富, 张业迪. 基于二元决策图的二值神经网络定量分析方法. CN: CN113378009A, 2021-09-10.
[3] 宋富, 赵哲, 陈光科. 一种基于攻击成本的对抗样本检测方法. CN: CN112381152A, 2021-02-19.
[4] 宋富, 赵哲, 陈光科. 一种基于样本鲁棒性差异的对抗样本检测方法. CN: CN112381150A, 2021-02-19.
[5] 宋富, 高鹏飞, 谢弘毅. 一种基于图同构的程序高阶功耗侧信道安全性的证明方法. CN: CN112364392A, 2021-02-12.
[6] 任洁, 严伟, 宋富, 高小平. 超导抗旁路攻击加密装置及加密方法. 202110178609.8, 2021-02-09.
[7] 宋富, 高鹏飞, 谢弘毅. 一种基于GPU的模型计数及其约束的求解方法. CN: CN112131583A, 2020-12-25.
[8] 宋富, 高鹏飞, 谢弘毅. 一种基于分治的程序高阶功耗侧信道安全性的证明方法. CN: CN112134729A, 2020-12-25.
[9] 宋富. 一种抗功耗侧信道攻击对策验证方法. CN: CN108809622A, 2018-11-13.

   

[1] Zhang, Yedi, Zhao, Zhe, Chen, Guangke, Song, Fu, Chen, Taolue. Precise Quantitative Analysis of Binarized Neural Networks: A BDD-based Approach. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY[J]. 2023, 32(3): http://dx.doi.org/10.1145/3563212.
[2] 宋富. 密码实现安全形式化验证发展现状与展望. 前瞻科技. 2023, 2(1): 90-105, http://lib.cqvip.com/Qikan/Article/Detail?id=7109340611.
[3] Sun, Pu, Chen, Sen, Fan, Lingling, Gao, Pengfei, Song, Fu, Yang, Min. VenomAttack: automated and adaptive activity hijacking in Android. FRONTIERS OF COMPUTER SCIENCE[J]. 2023, 17(1): 187-204, [4] 杨珉, 张超, 宋富, 张源. 系统软件安全专题前言. 软件学报[J]. 2022, 33(6): 1959-1960, http://lib.cqvip.com/Qikan/Article/Detail?id=7107361356.
[5] Gao, Pengfei, Xu, Yongjie, Song, Fu, Chen, Taolue. Model-based automated testing of JavaScript Web applications via longer test sequences. 中国计算机科学前沿:英文版[J]. 2022, 16(3): 53-66, http://lib.cqvip.com/Qikan/Article/Detail?id=7107388008.
[6] Liu, WanWei, Song, Fu, Zhang, TangHaoRan, Wang, Ji. Verifying ReLU Neural Networks from a Model Checking Perspective. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY[J]. 2020, 35(6): 1365-1381, http://lib.cqvip.com/Qikan/Article/Detail?id=7103652900.
[7] Gao, Pengfei, Zhang, Jun, Song, Fu, Wang, Chao. Verifying and Quantifying Side-channel Resistance of Masked Software Implementations. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY[J]. 2019, 28(3): http://dx.doi.org/10.1145/3330392.
[8] Xu, Zhiwu, Ren, Kerong, Song, Fu, IEEE. Android Malware Family Classification and Characterization Using CFG and DFG. 2019 13TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2019)null. 2019, 49-56, http://dx.doi.org/10.1109/TASE.2019.00014.
[9] Fu Song. Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks. nternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2019, [10] Pan, Haiyu, Song, Fu, Cao, Yongzhi, Qian, Junyan. Fuzzy Pushdown Termination Games. IEEE TRANSACTIONS ON FUZZY SYSTEMS[J]. 2019, 27(4): 760-774, [11] Fu Song. T-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language. International Conference on Theoretical Aspects of Software Engineering. 2019, [12] Zhang, Yedi, Song, Fu, Chew, Taolue. Making Agents' Abilities Explicit. IEEE ACCESS[J]. 2019, 7: 101804-101819, http://dx.doi.org/10.1109/ACCESS.2019.2931514.
[13] Fu Song. roid Malware Family Classification and Characterization Using CFG and DFG. International Symposium on Theoretical Aspects of Software Engineering. 2019, [14] Song, Fu, Zhang, Yedi, Chen, Taolue, Tang, Yu, Xu, Zhiwu, AAAI. Probabilistic Alternating-Time mu-Calculus. THIRTY-THIRD AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTY-FIRST INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE / NINTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCEnull. 2019, 6179-6186, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000486572500087.
[15] Fu Song. rifying and Quantifying Side-Channel Resistance of Masked Software Implementations. ACM Transactions on Software Engineering and Methodology. 2019, [16] Wang Feng, Song Fu, Zhang Min, Zhu Xiaoran, Zhang Jun, IEEE. KRust: A Formal Executable Semantics of Rust. PROCEEDINGS 2018 12TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2018)null. 2018, 44-51, http://dx.doi.org/10.1109/TASE.2018.00014.
[17] Song, Fu. Analyzing pushdown systems with stack manipulation. INFORMATION AND COMPUTATION[J]. 2018, 259: 41-71, http://dx.doi.org/10.1016/j.ic.2017.12.003.
[18] Zhang Jun, Gao Pengfei, Song Fu, Wang Chao, Chockler H, Weissenbacher G. SCINFER: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks. COMPUTER AIDED VERIFICATION, CAV 2018, PT IInull. 2018, 10982: 157-177, [19] Chen Taolue, He Jinlong, Song Fu, Wang Guozhen, Wu Zhilin, Yan Jun, Chockler H, Weissenbacher G. Android Stack Machine. COMPUTER AIDED VERIFICATION, CAV 2018, PT IInull. 2018, 10982: 487-504, [20] Zhang, Yueling, Zhang, Min, Pu, Geguang, Song, Fu, Li, Jianwen. Towards backbone computing: A Greedy-Whitening based approach. AI COMMUNICATIONS[J]. 2018, 31(3): 267-280, https://www.webofscience.com/wos/woscc/full-record/WOS:000432544800004.
[21] 张业迪, 宋富. 异构多智能体系统模型检查. 软件学报[J]. 2018, 29(6): 1582-1594, http://lib.cqvip.com/Qikan/Article/Detail?id=675408083.
[22] Lei, Yusi, Song, Fu, Liu, Wanwei, Zhang, Min. On the complexity of omega-pushdown automata. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2017, 60(11): https://www.webofscience.com/wos/woscc/full-record/WOS:000417334600008.
[23] Zhang, Yueling, Li, Jianwen, Zhang, Min, Pu, Geguang, Song, Fu, IEEE. Optimizing Backbone Filtering. PROCEEDINGS 11TH 2017 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE)null. 2017, 39-46, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000426968400006.
[24] Yusi LEI, Fu SONG, Wanwei LIU, Min ZHANG. On the complexity of ω-pushdown automata. 中国科学：信息科学（英文版）[J]. 2017, 60(11): 152-166, http://lib.cqvip.com/Qikan/Article/Detail?id=673606479.
[25] Chen Taolue, Song Fu, Wu Zhilin, Duan Z, Ong L. Model Checking Pushdown Epistemic Game Structures. FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2017null. 2017, 10610: 36-53, [26] Fu Song. Reasoning about Periodicity on Infinite Words. Symposium on Dependable Software Engineering (SETTA). 2017, [27] Xu, Zhengzi, Chen, Bihuan, Chandramohan, Mahinthan, Liu, Yang, Song, Fu, IEEE. SPAIN: Security Patch Analysis for Binaries Towards Understanding the Pain and Pills. 2017 IEEE/ACM 39TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE)null. 2017, 462-472, [28] 吴志林. Tractability of separation logic with inductive definitions: Beyond lists. International Conference on Concurrency Theory (CONCUR). 2017, [29] Chen Taolue, Song Fu, Wu Zhilin, Bowen JP, Liu Z, Zhang Z. Formal Reasoning on Infinite Data Values: An Ongoing Quest. ENGINEERING TRUSTWORTHY SOFTWARE SYSTEMS (SETSS 2016)null. 2017, 10215: 195-257, [30] 吴志林. Verifying pushdown multi-agent systems against strategy logics. International Joint Conference on Artificial Intelligence (IJCAI 2016). 2016, [31] Song, Fu, Wu, Zhilin. On temporal logics with data variable quantifications: Decidability and complexity. INFORMATION AND COMPUTATION[J]. 2016, 251: 104-139, http://dx.doi.org/10.1016/j.ic.2016.08.002.
[32] Chen Taolue, Song Fu, Wu Zhilin, AAAI. Global Model Checking on Pushdown Multi-Agent Systems. THIRTIETH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCEnull. 2016, 2459-2465, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000485474202070.
[33] Fu Song. Survey on Formal Models to Reason about Infinite Data Values. Journal of Software. 2016, [34] Song, Fu, Touili, Tayssir. Model-checking software library API usage rules. SOFTWAREANDSYSTEMSMODELING[J]. 2016, 15(4): 961-985, https://www.webofscience.com/wos/woscc/full-record/WOS:000384535800004.
[35] Fu Song. On reachability analysis of pushdown systems with transductions: Application to boolean programs with call-by-reference. the 26th International Conference on Concurrency Theory. 2015, [36] 吴志林. On the Satisfiability of Indexed Linear Temporal Logics. 26th International Conference on Concurrency Theory (CONCUR 2015). 2015, [37] Song, Fu, Touili, Tayssir. Model checking dynamic pushdown networks. FORMAL ASPECTS OF COMPUTING[J]. 2015, 27(2): 397-421, http://dx.doi.org/10.1007/s00165-014-0330-y.
[38] Fu Song. Model-checking for android malware detection. the 12th Asian Symposium on Programming Languages and Systems. 2014, [39] 吴志林. Extending Temporal Logics with Data Variable Quantifications. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). 2014, [40] Song, Fu, Touili, Tayssir. Efficient CTL model-checking for pushdown systems. THEORETICAL COMPUTER SCIENCE[J]. 2014, 549: 127-145, http://dx.doi.org/10.1016/j.tcs.2014.07.001.
[41] Song, Fu, Touili, Tayssir. Pushdown model checking for malware detection. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER[J]. 2014, 16(2): 147-173, https://www.webofscience.com/wos/woscc/full-record/WOS:000209673000003.
[42] Song Fu, Touili Tayssir, Piterman N, Smolka SA. LTL Model-Checking for Malware Detection. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013null. 2013, 7795: 416-431, [43] Fu Song. Pommade: pushdown model-checking for malware detection. the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering. 2013, [44] Fu Song. Efficient malware detection using model-checking. the 18th International Symposium on Formal Methods. 2012, [45] Song Fu, Touili Tayssir, IEEE. PuMoC: A CTL Model-Checker for Sequential Programs. 2012 PROCEEDINGS OF THE 27TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE)null. 2012, 346-349, [46] Song Fu, Touili Tayssir, Flanagan C, Konig B. Pushdown Model Checking for Malware Detection. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2012null. 2012, 7214: 110-125, [47] Song, Fu, Touili, Tayssir, Katoen, JP, Konig, B. Efficient CTL Model-Checking for Pushdown Systems. CONCUR 2011: CONCURRENCY THEORYnull. 2011, 6901: 434-+, 

   

（ 1 ） 恶意软件静态分析与检测关键技术研究, 主持, 国家级, 2015-01--2017-12
（ 2 ） 二进制程序的模型检查技术研究, 主持, 省级, 2015-01--2016-12
（ 3 ） 复杂二进制程序静态分析及其应用研究, 主持, 省级, 2014-07--2016-06
（ 4 ） 大规模概率并发实时系统模型检验, 参与, 国家级, 2016-01--2020-12
（ 5 ） 不确定环境下可信国产城轨控制系统（iCMTCt）构造关键技术研究, 参与, 国家级, 2015-01--2016-12
（ 6 ） 车载网和车载云中信息安全与隐私保护关键技术研究, 参与, 国家级, 2016-01--2019-12
（ 7 ） 汽车电子功能安全体系设计及功能安全模型及验证工具开发, 参与, 国家级, 2014-01--2016-11

（1）Verifying Pushdown Multi-Agent Systems against Strategy Logics   2016-07-09
（2）On reachability analysis of pushdown systems with transductions: Application to boolean programs with call-by-reference   2015-09-01

详见 https://songfu1983.github.io/