重要消息
論壇組織：
申文博、常瑞、周亞金
時間：2020年11月21日(星期六)
13:30-17:00
地點：富力假日酒店宴會廳3。
會議注冊：
http://chinasoft2020.cqu.edu.cn/hyzc.htm
預定酒店：
http://ccf.chinasoft2020.85do.com/
論壇議程：
| 時間 | 主題 |
| 13:30-14:20 | 技術報告 - 陳海波報告題目：軟硬體協同的系統安全增強技術研究報告摘要：Meltdown/Spectre、Rowhammer等新型硬體安全漏洞以及AI在安全攻防領域的廣泛應用使得目前計算機系統面臨巨大的安全威脅。該報告将回顧目前計算機系統面臨的安全挑戰，并且分析目前硬體安全擴充與AI帶來的安全增強機會，并介紹目前國際學術界以及上海交大IPADS團隊在系統安全方面的一些工作，并且展望未來的研究方向。 |
| 14:20-15:10 | 技術報告 - 秦承剛 報告題目：可信基礎設施的實踐 報告摘要：螞蟻集團在2020年雙11實施了可信安全容器叢集，通過安全容器、資料加密、可信啟動等技術初步實踐了可信基礎設施。同時，在積極探索通過軟硬體結合持續提升金融資料中心的隔離性、機密性與完整性。此次論壇以螞蟻在作業系統、安全沙箱、硬體加速、可信根等系統安全技術上的實踐為基礎，像大家介紹工業界在系統安全領域的最新進展。 |
| 15:10-15:20 | 茶歇 |
| 15:20-16:10 | 技術報告 – 宋富 報告題目：Formal Verification of Masking Countermeasures for Arithmetic Programs 報告摘要：Cryptographic programs may be vulnerable to practical power side-channel attacks, which may infer private data via statistical analysis. To thwart these attacks, several masking schemes have been proposed, giving rise to effective countermeasures for reducing the statistical correlation between private data and power consumptions. However, designing effective masking programs is a labor intensive and error-prone task. Existing formal verification approaches either are currently limited to Boolean programs or suffer from low accuracy. In this work, we propose an approach for formally verifying masking countermeasures of arithmetic programs. Our approach is essentially a synergistic integration of type inference and model-counting based methods. The type inference system allows a fast deduction of leakage-freeness of most intermediate computations, the model-counting based methods accounts for completeness. A distinguished feature of our type system lies in its support of compositional reasoning when verifying programs with procedure calls, so the need of inlining procedures can be significantly reduced. We have implemented our methods in a verification tool QMVERIF which has been extensively evaluated on cryptographic benchmarks including full AES, DES and MAC-Keccak. The experimental results demonstrate the effectiveness and efficiency of our approach, especially for compositional reasoning. In particular, our tool is able to automatically prove leakage-freeness of arithmetic programs for which only manual proofs exist so far; it is also significantly faster than the state-of-the-art tools: EasyCrypt on common arithmetic programs, QMSINFER, SC Sniffer and maskVerif on Boolean programs. |
| 16:10-17:00 | 技術報告 – 趙永望 報告題目：作業系統安全形式化驗證技術與應用 報告摘要：安全攸關作業系統主要應用于航空、航天、軌道交通、無人系統等領域，它位于計算機系統軟體棧的底層，作業系統的錯誤可能導緻系統奔潰、被攻擊等問題，涉及功能安全和資訊安全等問題。作業系統功能結構複雜，多核多任務的并發度高，開發與調試都十分困難，一些隐藏的錯誤用常見的軟體測試技術難以發現，而形式化驗證可幫助軟體開發人員發現深層的錯誤，確定作業系統的高安全可靠性。本報告主要讨論作業系統形式化驗證的背景意義、國内外現狀和面臨的挑戰，介紹我們提出的系統方法、理論技術以及工業應用實踐。 |
嘉賓簡介：
陳海波，上海交通大學特聘教授，并行與分布式系統研究所所長，領域作業系統教育部工程研究中心主任，國家傑出青年基金獲得者、ACM傑出科學家。主要研究領域為作業系統和系統安全。曾獲教育部技術發明一等獎(第一完成人)、CCF青年科學家獎、全國優秀博士學位論文獎等。目前擔任ACM SIGOPS ChinaSys主席、CCF系統軟體專委會副主任、ACM旗艦雜志《Communications of the ACM》中國首位編委與Special Sections領域共同主席、《ACM Transactions on Storage》編委。曾任ACM SOSP 2017年大會共同主席、ACM CCS 2018系統安全領域主席、ACM SIGSAC獎勵委員會委員。按照csrankings.org的統計，其在作業系統領域近5年(2015-2019)發表的高水準會議(SOSP/OSDI, EuroSys, Usenix ATC和FAST)論文數居世界第一。
秦承剛，螞蟻集團資深技術專家，任職于可信原生技術部，帶領可信硬體與核心團隊，專注在可信金融基礎設施的技術創新與研發工作，涉及作業系統/安全容器等系統軟體及軟硬體結合領域。在ASPLOS，SoCC等學術會議上發表過多篇論文。
Fu Song is an Assistant Professor at School of Information Science and Technology in the ShanghaiTech University. Fu received his Ph.D. from University Paris Diderot (Paris 7) in 2013. He was an Associate Research Professor and Lecturer at School of Computer Science and Software Engineering in the East China Normal University during 2013-2016, and a visiting researcher at Computer Security Lab of Nanyang Technological University in 2014. His research spans formal verification, program analysis and cyber-security. Fu has published more than 50 papers in peer-reviewed conferences and journals including CAV、ICSE、ISSTA、, IEEE S&P、AAAI、IJCAI、I&C, IEEE TSE and ACM TOSEM. He has been the recipient of the EASST best paper award at ETAPS 2012、Shanghai Pujiang Talent and Shanghai Chenguang Scholar.
趙永望 浙江大學 教授、博導，擔任ARINC653國際作業系統标準委員會委員、國際資訊技術安全評估标準(Common Criteria,CC)作業系統核心技術委員會委員、CCF系統軟體專委會和形式化方法專委會委員。主要研究方向包括作業系統安全、形式化驗證、程式設計語言等。提出了作業系統形式驗證的系統性理論和方法，突破了覆寫單核到多核、标準到産品、模型到源碼的形式化驗證關鍵技術，完成了10多個國内外作業系統的形式驗證工作，顯著提升國産系統的安全可靠性。相關研究成果得到美國波音、法國空客和國際知名實時作業系統廠商的認可，被納入國際标準，并在開源實時作業系統社群産生影響力。
論壇組織：
申文博，浙江大學百人計劃研究員，博士生導師。2015年獲得美國北卡羅萊納州立大學計算機博士學位，研究方向為系統及無線安全，并于同年加入位于美國矽谷的三星美國研究院(Samsung Research America)，擔任作業系統核心安全的技術負責人。于2019年加入浙江大學網絡空間安全研究中心和計算機科學與技術學院。申文博研究員研究成果包含論文及專利30餘篇，覆寫全部計算機安全四大國際會議，獲得2項傑出論文獎，包含四大頂級會議之一的NDSS的傑出論文獎。申文博研究員常年活躍于移動系統安全攻防的第一線，通過分析實際攻擊，設計相應的作業系統保護方案，具有學術界和工業界的雙重研究經曆和視野；多年來設計、實作并主導部署了多種作業系統核心安全機制，保護超過億部裝置系統核心安全。
常瑞，副教授，博士生導師，浙江大學。從事系統安全方向的科研與教學十餘年，于解放軍資訊工程大學獲得計算機科學與技術博士學位，并獲ACM中國優秀博士學位論文分會獎。研究興趣圍繞嵌入式系統安全，研究方向包括可信執行環境安全防護、系統安全加強、形式化分析與驗證、邊緣計算安全等，現任國家資訊标準委員會專家、IEEE 可信裝置擴充标準項目副主席(P2811.6)，近三年發表相關學術論文四十餘篇。加入浙江大學前曾就職于中國人民解放軍資訊工程大學，期間多項研究成果獲得省部級以上獎勵(省部級教學成果一等獎1項、省部級科技進步二等獎2項等)，教學方面獲得全國微課競賽二等獎、省部級一等獎等，被評為全軍優秀教師。
周亞金老師(個人首頁：https://yajin.org/)是浙江大學網絡空間安全學院/計算機學院百人計劃研究員(博導)。周老師于2015在美國北卡州立大學獲得博士學位，随後擔任奇虎360進階安全研究員，從事移動安全産品研發工作。2018年加入浙江大學。他發表了40多篇學術論文，包括安全四大會議10篇，四次獲得最佳論文獎，包括EURO S&P 2019(國内首次)。他的研究具有較大的影響，總引用數超6500次，h-index 17。兩篇文章入選自1981年以來全球引用最多的安全論文前100篇清單。入選AMiner 2009到2019年全球安全和隐私領域最有影響力的100位研究者清單(排名48)。作為指導老師之一，參加美國國立衛生部主辦的2019 iDash全球基因安全計算SGX賽道，開發的基于硬體的隐私機器學習系統性能比第二名領先數十倍，以絕對優勢獲得全球第一名(國内首次)。他受邀擔任過個頂級安全學術會議的程式委員會委員，包括CCS, IEEE S&P以及EURO S&P。他的研究工作得到了華爾街日報、中央電視台等媒體報道和谷歌、facebook、三星等企業的緻謝。