隨著軟體應用滲透日常生活的各個領域，軟體的高可靠與高安全受到廣泛關注。程序設計語言作為軟體的表示載體和描述工具，對軟體的開發效率和開發質量起決定性作用。本論壇將討論如下問題：1）如何設計安全的程序設計語言？2）如何提供安全加強的軟體開發環境？3）如何進行安全的編程？
如需觀看需要註冊 CCF 帳戶報名，官方訪問連結：
https://conf.ccf.org.cn/web/html15/dayMeetZhibo.html?dayMeetNewsId=8a9e362c7af1ba09017af25055c00001&globalId=m8271748750546083841617255458379
或點擊文末 閱讀原文 跳轉
時間：12 月 17 日 13:30-17:30
地點：在線會議室 v6
時間報告題目講者13:00 - 13:25安全C語言設計與實現左志強13:25 - 13:50從程序驗證到「開發即安全」曹欽翔13:50 - 14:15指令編碼解碼的形式化驗證方法汪宇霆14:15 - 14:40密碼程序安全威脅與形式驗證宋富14:40 - 15:05面向企業級微服務架構程序分析的IR設計狄鵬賀飛
清華大學長聘副教授，博士生導師，CCF形式化專委會常務委員
主要研究程序驗證理論、方法、工具及應用。開發了模型檢測和軟體驗證工具，並應用於航空、航天、高鐵等國家重大安全領域。在包括POPL, CAV, PLDI, OOPSLA, ICSE, ESEC/FSE, ASE等在內的國際重要會議和期刊上發表論文70餘篇。主持和參與國家973項目、自然科學基金重大項目、科技支撐計劃項目、重點研發項目等10餘項。任《Theory of Computing Systems》編委，CONCUR, FMCAD, SAT, APLAS, ICECCS, SETTA等國際學術會議程序委員會委員。
擔任ARINC653國際作業系統標準委員會委員、中國計算機學會(CCF)高級會員、CCF系統軟體專委會和形式化方法專委會委員。曾任國際標準化組織 ISO/IEC JTC1 SOA研究組組長、新加坡南洋理工大學高級研究員。主要研究方向包括作業系統安全、形式邏輯與驗證、程式語言原理等。主持和參與國家自然基金重點項目、核高基重大專項、重點研發計劃等項目十餘項，2011和2017年分別獲得中國電子學會和山東省科技進步一等獎。
報告題目：安全C語言設計與實現
報告摘要：進入資訊時代，軟體已然成為現代社會的重要基礎設施。確保軟體安全可信，對維護信息安全以及社會生產具有重要意義。然而隨著軟體功能日趨複雜，規模日益增大，軟體的安全可信面臨愈加嚴峻的挑戰，如何確保大規模軟體的安全性，已然成為學術界、企業及政府高度關注的課題。本次報告重點介紹我們在安全C語言設計與實現方面的工作。在已有C語言的基礎上，通過增加新類型，並結合動態、靜態分析及編譯技術，最終在程式語言與編譯器層面保證軟體安全。
個人簡介：於新加坡國立大學獲博士學位，曾在美國加州大學歐文分校從事博士後研究。科研工作聚焦於系統軟體的可信保障與優化，在系統化程序分析、軟硬體協同的編譯器優化設計等方面取得重要進展，創新性工作以第一和通訊作者發表在包括PLDI、OOPSLA、EuroSys、ACM TOCS等國際重要學術會議和期刊上；獨立研發並開源多個系統軟體分析及優化系統，並已在華為、阿里等多個企業成功實現轉化與應用；擔任PLDI2022、FSE2022、IEEE TSE等多個國際重要學術會議程序委員及期刊審稿人。
曹欽翔
上海交通大學約翰霍普克洛夫特計算機科學中心助理教授、博導
報告題目：從程序驗證到「開發即安全」
報告摘要：交互式定理證明技術是驗證程序複雜性質的重要手段，其主要思想是在現有自動化驗證工具無力完成驗證工作的情況下，由人提供額外信息從而輔助驗證工具「理解」程序並驗證其功能以及安全性。經過探索，這一程序驗證技術可以嵌入程序開發環境，從而實現「開發即安全」。本報告將介紹 Verified Software Toolchain（VST）工具，該工具以交互式定理證明技術為基礎，集成了學術界在程序邏輯等諸多方面的理論研究前沿成果，可用於驗證複雜 C 語言程序的功能正確性與安全性，排查空指針引用漏洞、緩衝區溢出錯誤、並發數據訪問競爭等各種問題。
個人簡介：曹欽翔，本科畢業於北京大學，博士畢業於美國普林斯頓大學，2018年回國任教，現為上海交通大學約翰霍普克洛夫特計算機科學中心助理教授、博導。其長期從事基於交互式定理證明的程序驗證工具開發，並研究有關程序邏輯特別是分離邏輯的理論問題。曹欽翔是Verified Software Toolchain（VST）工具的主要開發者之一，首次實現了從業務邏輯，到原始碼開發，再到編譯的全鏈條正確性驗證。
汪宇霆
上海交通大學John Hopcroft計算機科學中心副教授
報告題目：指令編碼解碼的形式化驗證方法
報告摘要：機器指令的編碼和解碼規範是計算機體系結構中不可或缺的組成部分，從中衍生出的編碼解碼算法被廣泛應用於各類處理機器代碼的程序，包括編譯器、彙編器、二進位程序分析軟體等。使用形式化方法保障指令編碼解碼的正確性，對於從根本上提高這些程序的可靠性有重要意義。已有的該類方法存在一個本質缺陷：它們基於傳統的、允許二義性的詞法和語法分析，無法保證編碼和解碼算法互為逆過程，而這個性質對於確保二進位機器碼運行的正確性至關重要。該問題導致已有的指令編碼解碼驗證結果無法被應用於大多數實際程序。我們提出了一種新型的機器指令規約語言CSLED，其基於一種不帶二義性的指令規約模型，可精確表達複雜體系結構中的指令格式。在此基礎上，我們提出了一系列算法，從該語言描述的指令規約中自動提取編碼解碼過程，以及兩者互為逆過程的形式化證明。該方法已被成功應用於驗證CompCert可信編譯器的X86彙編器後端。
個人簡介：上海交通大學John Hopcroft計算機科學中心副教授，此前於美國耶魯大學計算機系擔任博士後研究員，博士畢業於美國明尼蘇達大學雙城分校。長期從事形式化方法方面研究，內容涵蓋形式化驗證和程序設計語言的理論基礎（包括證明論、類型論、邏輯框架等）以及它們在關鍵性系統軟體（如編譯器和作業系統）中的應用，代表性研究成果以發表於形式化驗證和程序設計語言的頂級國際會議（如POPL、CAV、OOPSLA、ESOP等）。此外，還致力於開發基於證明理論的定理證明工具，作為主要設計人員之一參與開發了基於高階抽象語法的新型定理證明工具Abella（http://abella-prover.org），其已被成功應用於程序設計語言學術界的多個研究項目。
報告題目：密碼程序安全威脅與形式驗證
報告摘要：本報告介紹密碼程序實現所面臨的安全威脅，包括時間側信道、功耗側信道、緩存側信道、故障注入等，總結面向安全威脅的形式驗證技術與挑戰，最後探討我們的一些想法。
個人簡介：宋富，上海科技大學常任副教授、研究員、博導，系統與安全中心主任。宋富博士於2013年4月獲得巴黎大學（原巴黎狄德羅大學）計算機科學博士學位，同年8月加入華東師範大學任講師，2016年1月破格晉升為副研究員，於2015年分別榮獲上海市「浦江人才」和上海市「晨光學者」稱號。2016年8月全職加入上海科技大學信息科學與技術學院，擔任tenure-track助理教授、研究員，2021年7月晉升為常任副教授。研究領域包括模型檢驗、程序分析與驗證、系統和AI安全，已在國際一流期刊和會議發表60多篇論文，如：IEEE TSE, ACM TOSEM, CAV, ICSE, ISSTA, S&P等。
報告題目：面向企業級微服務架構程序分析的IR設計
報告摘要：微服務是面向服務體系結構的最新發展趨勢和研究熱點，已經在工業實踐中形成了廣泛的應用。據統計，螞蟻集團在2019年一年就提交了4億行的基於微服務的代碼。因此，微服務應用的安全性和可靠性時時刻刻影響著每一位網際網路用戶，正受到日益增長的關注。然而，作為軟體安全的重要手段，程序分析往往難以應用到企業級微服務中，這是由系統的複雜性和龐大的代碼量導致。Yannis在PLDI『20就曾指出當前並沒有一個很好的程序分析算法或框架，能在企業級微服務應用上得到一個全面令人滿意的結果。針對這一問題，我們根據在螞蟻大規模程序數據的實戰經驗，構思通過構建面向微服務的輕量彈性中間表達，重構數據驅動的微服務程序分析能力，滿足可擴展性、多語言支持、基礎分析模塊化復用、開放生態等能力，並應用於工業DevSecOps的開發流程中。未來希望能依此為基礎，形成新的開發模式生態。我們非常高興能分享在螞蟻程序分析的經驗，並將挑戰問題和同業者探討。
個人簡介：狄鵬，螞蟻技術研究院可靠計算和軟體工程實驗室研究員，中國科學院兼職研究員，澳大利亞新南威爾斯大學兼職高級講師。狄鵬博士研究軟體領域多年，其研究成果近年連續發布在PLDI、Micro等頂級學術會議。狄鵬和他的團隊致力於研究軟體分析、安全、可靠性等領域的前沿課題，聚焦打造螞蟻新一代面向雲側企業級應用的軟體分析研發系統，為螞蟻集團數億行代碼構成的複雜軟體系統的安全性保駕護航，並構建新一代的DevSecOps開發生態，提高雲應用安全開發的效率。