CNCC 2022 参会小记
借着刚刚成为的 CCF 学生分会执行委员的身份，第一次参加中国计算机大会，可惜是线上。报名了三个和 PL / SE / Security 相关的论坛和一个博士培养的论坛，希望能给自己的毕设和未来发展带来一些启发。
开幕式
感觉没啥意思，主要介绍了主办地贵州和贵州大学，紧随其后的“从网格到算力网络”论坛也很有当地特色。
An Overview of High Performance Computing and Future Requirements - Jack Dongara
- 中国拥有 / 制造了世界上最多的超级计算机(151 / Top 500)
- Future Benchmark: Floating operation(HPL) -> Moving data(HPCG)
- How to build a more balanced system
- Quantum computing used as accelerator, not a replacement of computing machine
- HPCs are now dominated by X86 Arch, small impact from ARM, no RISC-V
- Advice for young people:
- follow your passion
- try yourself challenging task, prepare to fail
- interacted with others
数字技术推动经济增长：数据全纳与效率倍增
近十年经济下行(10% -> 5%)的主要原因是服务业的劳动效率没有增加，疫情只是波动因素：2015 年，中国的服务业增加到 50% 以上，但服务业中大部分的非技术部门，需要的是定制化 / 个性化的服务，从而没有提高效率；相比之下，制造业的生产效率由于技术提高，趋势更加显著。
数据驱动的开源漏洞挖掘与修复
Forrester 研究表明：应用软件 80%~90% 的代码已来自于开源组件。开源供应链为企业提供了大量“免费午餐”，但开源漏洞的存在也给企业带来了严峻的安全风险。开源漏洞层出不穷，一个小小的安全漏洞（如 Log4j 远程代码执行漏洞）却足以搅动整个软件或互联网产业发生地震（进行大面积库升级或替换以缓解安全危机）。开源漏洞从“被初始发现”到“被用于针对企业项目进行漏洞预警与治理”之间仍存在较大的空档期。而该空档的存在，恰恰成为了黑客利用开源漏洞作案的绝佳时机。基于“开源大数据”进行智能挖掘与洞察，快速感知开源安全漏洞并进行精准漏洞影响范围通知及安全响应，可大大降低上述时间空档并成为未来开源组件使用场景的有力安全保障。
本论坛将围绕开源漏洞挖掘、漏洞信息精化、漏洞智能修复相关技术组织最新技术分享与研讨，如开源安全现状分析、1-day / 0-day 开源漏洞挖掘及识别技术、开源漏洞精准影响分析技术、开源漏洞治理技术、二级制代码开源漏洞定位技术等。
开源安全：挑战、解决方案和机遇 - Liu Yang
开源安全的挑战
- 软件吞噬世界 -> 开源吞噬软件：60-90% 的软件代码属于开源代码；每天有1w个新的开源代码包；每个开源组件平均依赖8个其他的开源组件。
- 开源组件的许可证的限制
- 在不知情的情况下就引入了有漏洞的第三方代码包（二进制，源代码，容器等）
- 开源漏洞数据库（NVD）的不准确
开源的解决方案
- MVP：通过克隆的思路进行代码层面的漏洞匹配
- 漏洞函数和补丁函数相似，gap很小，难以区分
- 包含了很多无关的代码，影响了相关性检测
后面听不清了。。。
面向公开 / 隐匿开源漏洞的智能化分析与挖掘技术 - 梁广泰
宏观趋势：
- 数字化转型：上云
- 应用交付的上线越来越快，安全应用保证能力持续左移 e.g. 美国商务部新规：未经审批禁止向中国分享安全漏洞
- 主流云服务商都启动了 SCA 能力，成为 DevSecOps 标配
- 漏洞在披露之前已经在开源社区进行了修复，从而产生了补丁和相关数据
CVE 公开漏洞分析技术
CVE 报告以自然语言描述为主，结构化程度欠佳，所包含的漏洞包范围尚未精确描述，无法直接进入自动化处理 e.g. 该漏洞只影响到了 xxx 版本
- ICPC 2022 公开漏洞智能精化技术：多标签学习面临样本不够的问题，尤其是处于长尾部分的 label
- Deep Learning 的技术是可以带来有效性提升的
面对 zero-shot 的场景，华为云提出了软件族的概念，软件之间拥有相同的实现逻辑。使用了 漏洞-包版本 的自动化映射算法。
隐匿漏洞补丁识别技术
TDSC 2022 隐匿漏洞分析技术：基于 code change，提取 AST，加入到 embedding 中，判断当前的补丁是否在修复漏洞
数据库软件安全漏洞测试技术 - 姜宇
针对于数据库，SQL 语句逻辑的测试
- Sqlancer：生成 DBMS 会优化查询 SQL 语句
- Squirrel：覆盖率导向的模糊测试，利用 IR 将语法正确和语义感知的 SQL 引入模糊测试
- Translate to IR
- Syntax-Preserving Mutation
- Semantic-Guided with Data dependency
- 存在的问题：
- 生成复杂的 SQL 语句（方言）
- 缺陷分析成本：数据库的异常捕获
- 适配工业场景的时序数据库（IoTDB）
- WingFuzz-Ratel
开源漏洞在二级制代码中的定位技术 - 霍玮
《SYNOPSYS 2022 开源安全和风险分析报告》：软件漏洞会随着代码复用传播
如何识别上述情况：开源软件识别 -> 版本识别 -> 函数识别（可能只用了部分的代码）
二进制软件开源库检测
- 代码相似性检测 + 复用类型识别：
- 提取代码特征：抗编译优化的代码特征提取，选择能体现开源组件的核心功能和算法，且同时存在于二进制和源代码中。主要的三类特征：符号，常量数据（字符串，数组），控制流（if-else，switch）信息。从 .data，.rdata 段中提取。
- 代码特征匹配，不同特征使用不同的算法。二进制流熵算法，类 TF-IDF 的加权算法
- 复用类型识别：简单复用，部分复用，虚假的嵌套复用
实验对象：开源项目发布的二进制文件，百度软件中心的安装包
二进制软件开源库版本检测
- 版本敏感的特征：
- 软件级特征：衡量特征在开源软件版本间的差异（字符串和导出函数比较高）
- 函数级特征：函数中的赋值常量，函数中参数常量和函数调用图
不同版本在同一编译环境下的成功率比较低 -> 使用基于机器学习的特征提取
二进制函数相似性分析
C 语言的库使用不规范 -> 深度学习增益的二进制代码对比
数据驱动的开源代码漏洞治理 - 张源
- 公开漏洞库普遍存在漏洞版本信息错误的情况 -> 基于漏洞指纹的影响版本评估
- 公开漏洞库普遍缺乏用于评估漏洞危害的信息，PoC在漏洞数据库中的比例很低 -> 基于导向式模糊测试的 PoC 迁移，使 PoC 在不同版本中都能触发。使用高版本中的执行序列指导低版本 PoC 的生成
- 公开漏洞库普遍存在补丁信息数量少，质量低的情况 -> 基于代码变更（commits）排序的补丁定位，找补丁的搜索引擎
部署补丁是治理漏洞的主要方式，但上下游分支不对应 -> 面向上游软件多分支/下游软件制品的自动化补丁部署
下游软件系统需要很长时间才部署补丁，且大部分是闭源发布
供应链中开源软件的安全现状分析 - 董国伟
事件：Log4j 漏洞、高通和联发科芯片漏洞影响数百万设备、超 1200 个 NPM 包被滥用于挖掘门罗币、SocGholish JavaScript 攻击美国新闻媒体公司
奇安信《2022 软件供应链分析报告》，数据来自于其公司 SaaS 产品 - 代码卫士，对标 Coverity
领域特定语言与安全编程
软件安全性和开发效率一直是矛盾的问题。虽然存在程序验证、软件测试等多重手段来提升软件安全性，但达到较高的安全性级别需要付出较大的开发成本，在实践中往往不可接受。
领域特定语言是解决该问题的可能方向。领域特定语言针对特定领域的编程任务所设计，通过构造式的方式来避免特定类型的缺陷，使得在提升安全性的同时不增加（甚至减少）程序员的开发代价。但是，由于领域特定语言设计开发成本高，有额外学习代价，和通用编程语言的互操作成本较高等原因，在实践中应用范围仍然有限。本论坛将邀请从事领域特定语言研究和安全编程研究的专家，共同讨论采用领域特定语言来解决安全编程问题的前景和发展路线。
Active Learning for Software Rejuvenation - 沈嘉思
领域特定语言的敏捷开发及其支撑环境 - 胡振江
我们需要面向泛在计算（IoT，CPS，场景）的安全的编程语言及环境
SICP: computer itself is … constructing a … language
使用一种通用的核心语言来连接高级 DSL 和低级 DSL：包含计算规则，程序分析/测试，程序优化，代码生成，支撑环境
From functional programming to linear functional programming - Hongwei Xi
λ演算与基础软件 - 陈钢
λ演算是软件领域的微积分，λ演算支撑 DSL，DSL 支撑基础软件，基础软件支撑应用软件
- 带类型的数据描述语言：HERMIAS
- 现有 Json，YAML
- 缺乏类型和重用机制
从程序验证到安全编程 - 曹钦翔
计算机软硬件系统安全性形式化验证
计算机软硬件系统（比如自动驾驶系统与区块链）一方面与人们日常生活深度融合，关系到人民群众生命财产安全；一方面支撑航空航天、高铁等关键领域，直接影响国家安全。因此计算机软硬件系统的安全性愈发重要，要求越来越高。
形式化验证技术具有严格数学基础，包括定理证明、模型检验、约束求解、抽象解释等多种方法；经过多年发展，其已经成为保障计算机软硬件系统安全性的重要途径，并成功应用于航空航天控制软件、操作系统内核、编译器、硬件设计、网络协议等领域，从而受到学术界和工业界的广泛关注。
本论坛将邀请来自学术界和工业界的顶尖专家，共同探讨计算机软硬件系统安全性形式化验证的前沿理论、技术、与应用，并展望发展趋势。
计算机软硬件的复杂性增加：Apple M2 的晶体管数量，Linux 的项目代码数量
形式化验证：模型检测，定理证明，约束求解，抽象解释 e.g. 操作系统内核的验证 seL4，COMPCERT 的形式化编译器
系统安全形式化验证：从交互式到自动化 - 赵永望
系统安全：计算系统的安全，形式化方法成为系统安全保障的新模式
什么是形式化方法：基于严格数学基础对计算机软硬件系统进行描述、开发和验证的技术。使用逻辑公式，覆盖了所有可能的任意数组和执行分支。目前行业都使用交互式定理证明的方式。
seL4 操作系统微内核：源代码完全形式验证，功能正确性和信息流安全。投入了大量的验证时间、人力，使用了 20 多万行 Isabelle / HOL 交互式定理证明代码。
形式化验证成本：平均每人年产出 1 万行证明代码
形式化验证领域：航空航天，无人驾驶设备，区块链，物联网，网络安全，国内评估机构颁发首个最高等级的软件 EAL5+ 级别证书
形式化系统安全验证的下一阶段：自动化是重点
- 如何从 文档 / 标准 / 黑盒 系统自动生成形式化规约：基于 NLP 的结构化本体模型生成
- 如何对 规约 / 源码 进行自动形式化验证：使用 LLVM MLIR 处理不同的前端源代码（C，C++，Rust），在 LLVM IR 的层面做符号执行，转化为 Isabelle 的交互式证明代码
- 自动的形式化集成：Isabelle / Cloud，定理证明即服务（TPaaS）
后摩尔时代通过验证提升性能的工业实践 - 付明
形式化原本是保证安全性的，如何提高性能？
国王收税和三个形式化僧人的故事
后摩尔时代：通过改变半导体工艺来提高性能的几率越来越小，软件并发来获得更好的性能。但并发程序的验证和复现很复杂，且扩展性差。
- Relaxed memory model(RMMs)：ARM，RISC-V 不同于 X86，指令的内存访问行为不同，造成了并发场景下的问题
- CPU 的乱序执行
- Deep NUMA hierachies e.g. Linux 内核的同步原语： TTAS -> Ticketlock -> qspinlock -> CNA lock(NUMA awareness)
Facebook Infer 为什么能成功，集成到了 CI / CD 里面，Pay as you go
形式化人如何在工业界生存：verification 只是工具
Pratical Verification
目前很多的定理证明是不考虑并发时的弱内存情况的
目标：increate confidence，exhaustive as long as it pays off
VSync：不使用汇编来定义同步原语
面向应用的硬件模型检测技术 - 张弘策
逻辑电路中的形式化属性检查，SystemVerilog 断言
没有免费午餐：对于完全任意的优化问题，没有一种算法比随机搜索算法更优
硬件形式化验证的常见问题：是否正确实现了指令集功能，可以用组合状态机上的安全性质描述。利用模型检测进行指令功能检查通常只能得到有界证明，即在 X 个时钟周期内，功能是正确的；无界的证明依赖于归纳不变量，即使在规模较小的设计上，计算不变量也非常耗时。
从SAT到SMT - 蔡少伟
SAT
- SAT：布尔可满足性问题，给定一个命题逻辑，判断是否存在使其为真的赋值。一般会转化为合取范式（CNF）求解。第一个被证明为 NP 完全的问题。
- SAT 的应用：EDA 基础引擎，电路等价性验证，模型检测
- SAT 的求解：CDCL（子句学习） / 局部搜索，RELAXED 混合求解算法，算法从 1960 - 2020 一直在演进
- SAT 的现状：当代 SAT 求解器可在合理时间内求解百万变量级别的 SAT 问题
- SAT 的挑战：
- 对于特定的 SAT 问题，求解规模仍然很小，例如对于复杂电路等价性验证 UNSAT 证明，密码分析
- 有些现实中的 SAT 问题规模远超出百万变量，e.g. Kissat 的工程实现，SAT 比赛使用的串行算法的发展进入平缓期，机器学习用于 SAT 求解
- 并行算法求解 SAT
- SAT 的表达能力还不够 -> 使用 SMT
SMT
- SMT：限定背景理论的一阶逻辑公式
- SMT 应用：硬件模型检测，符号执行，软件验证，协议验证
- SMT 求解器：Z3，CVC5
基于抽象内存模型的C程序编译验证 - 汪宇霆
验证编译器功能的正确性，e.g. CompCert
- 基于区块的内存模型
- Nominal memory model
程序隐私安全性的形式验证 - 宋富
对程序的隐私安全进行威胁建模，一些侧信道的攻击
- JIT 时间侧信道安全形式证明
- JIT 时间平衡安全性形式定义
- 安全多方计算呢程序的安全性
处理器安全论坛
处理器硬件安全问题频发，“熔断”、“幽灵”、“骑士”、“闪电”等漏洞影响面广、危害大、修复困难，给现代信息网络基础设施安全带来前所未有冲击。本论坛面向安全处理器设计，从处理器硬件安全风险识别与检测、安全处理器架构设计与分析两个方面展开研讨。
处理器是网络信息安全空间的最后一道关闸，是上层网络信息系统的基石。长期以来，学术界和产业界以底层处理器硬件为“可信基”，如Intel SGX和ARM TrustZone等，认为其可信、安全，实际上形成了巨大的“安全盲区”，一旦这些处理器硬件出现安全漏洞，加解密算法赖以执行的可信硬件执行环境、以处理器为可信基的大量安全应用、以处理器为硬件基础的网络安全措施等，均失去根本基石，现有的网络空间安全秩序和体系架构面临被撼动的风险。
当前，主流处理器硬件漏洞频发，处理器设计过分追求高性能和低功耗而忽略安全性，是导致当前各种已发现处理器安全漏洞的主因。 “熔断”、“幽灵”以及各种变种主要利用了现代处理器广泛采用的“高性能”设计策略的安全缺陷，“骑士”、“闪电”等漏洞则主要利用处理器“低功耗”设计策略的安全缺陷，而针对SGX等设计策略缺陷的漏洞、针对片上调试系统设计缺陷漏洞（如“钉枪”）等，则与处理器现有安全功能设计缺陷相关。
面向未来安全处理器设计，本论坛将探讨如何识别与检测处理器硬件安全风险，如何考虑安全处理器架构设计等两个方面内容，论坛讨论与交流有利于促进领域研究人员对处理器安全问题的认识水平的提升。