2023夏季实习生技术项目回顾:从零知识电路到深度学习安全

本文详细介绍了Trail of Bits 2023年夏季实习生的七个核心技术项目,涵盖零知识电路确定性检查、Windows事件追踪模糊测试、GDB/pwndbg性能优化、大语言模型安全评估、密码学协议文档化、PyTorch安全研究以及定向模糊测试技术突破。

可扩展的Circom确定性检查工具Circomference

Xiangan He的夏季项目专注于构建一个工具,用于检查生产级零知识(ZK)电路中的约束缺失和非确定性问题。现有的安全工具在处理超过1000万约束的电路时能力有限,这促使了Circomference的开发。受Picus和Ecne等工具的启发,Circomference使用易于交换的SMT求解器后端,通过快速的Rust编排器和确定性传播器来审查现实场景中常见的大型复杂电路的确定性。

确定性检查对于识别零知识电路中的错误至关重要。Xiangan的项目证明,Circomference和Picus等工具能够在250个已知漏洞的ZK电路样本中检测出98.6%的漏洞。此外,由于改进了内存使用和传播启发式方法,Circomference能够轻松处理那些导致Picus迅速耗尽系统RAM的电路。

Circomference不仅在效率上表现出色,还能有效检测实际审计中使用的电路的非确定性,对于确保零知识电路的完整性和安全性具有不可估量的价值。

Windows事件追踪(ETW)模糊测试

Michael Lin的项目专注于对使用Windows事件追踪(ETW)消费事件的应用程序进行模糊测试。ETW在Windows系统中扮演关键角色,服务于各种组件和端点检测与响应(EDR)解决方案。然而,由于任何人都可以使用正确的GUID注册提供程序,这一过程容易受到利用。

Michael的团队首先选择感兴趣的EDR并进行逆向工程,以确定它们从哪些提供程序消费事件。由于现有的测试或模糊测试框架无法匹配ETW等进程间通信机制的复杂性,他们不得不开发自己的框架。

他们创建的模糊测试器旨在生成发送到这些提供程序的随机事件,以发现解析错误。在这个过程中遇到了有趣的挑战,包括难以绕过Windows进程保护和跟踪模糊测试进度。尽管如此,团队成功自动化了大部分过程,并计划将该方法应用于其他利用ETW的应用程序。

增强GDB和pwndbg

Matheus Borella的夏季项目涉及对GDB和pwndbg(一个用于逆向工程和漏洞开发的GDB插件)进行改进,特别注重提升性能和添加功能。

一个显著成就是显著减少了利用GDB索引的用户的调试器启动时间。这一变化在测试中展示了高达20倍的显著速度提升。此外,Matheus引入了为某些Python类型添加__repr__的功能,并提交了(尚未合并的)补丁,通过自定义类型创建和运行时符号添加来扩展Python API,增强了GDB的调试和逆向工程能力。

他们的工作还为pwndbg带来了多项生活质量改进,包括实验性的释放后使用检测和新命令(plist、stepuntilasm和break-if-[not-]taken)。在此过程中,他们甚至发现并修复了QEMU中的一个错误,该错误在某些情况下导致GDB崩溃。

评估大语言模型的安全性

Patrick Dobranowski的项目解决了评估大语言模型(LLM)在各个领域有效性的需求。Patrick的项目旨在创建一种方法,以便更轻松地确定哪些模型擅长哪些任务。在开发过程中,我们还注意到现有指标在Trail of Bits感兴趣的主题(如Solidity语言理解)方面存在不足。Patrick随后努力创建了一个从HumanEval扩展的评估框架,以评估Solidity代码理解能力。

通过ZKDocs赋能开发者

Sanketh Menda致力于解决密码学研究论文中描述的协议与相同协议实现之间的差距。特别是,他们专注于零知识证明,并为ZKDocs贡献了关于内积论证及其在多项式承诺方案中应用的内容,将这些协议提炼为基本的实现细节。

Sanketh还与密码学团队合作,对零知识相关代码库进行安全评估,获得了该领域的实践经验。

研究PyTorch的深度学习安全性

Kevin Chen的项目探索了PyTorch(一个广泛使用的Python深度学习框架)的正确性和安全性。虽然PyTorch以其简单性和高效性而闻名,但其复杂的内部工作机制引发了关于正确性的问题。

Kevin最初专注于PyTorch的自动微分引擎(称为autograd),这是神经网络训练的基础。他利用数据流分析和调试器进行的细致研究得出结论,PyTorch开发人员遵守关键规则。Kevin的工作揭示了PyTorch代码生成实践的见解,并确定了未来研究的潜在领域。

真正遵循指示的模糊测试器!

在定向模糊测试领域,工具使用如最短路径到目标等指标来发现特定代码位置,Sameed的工作脱颖而出。他的项目扩展了LibAFL,创建了一个能够真正遵循指示并生成满足一系列前提条件的输入的模糊测试器。

传统的可达性指标通常无法捕捉现实世界错误的复杂性,因为利用通常需要满足特定的前提条件序列。Sameed的创新方法采用一系列目标,并在取得进展时动态更新最短路径到目标的指标计算。这种方法使模糊测试器能够生成触发更复杂错误的输入,显著推动了定向模糊测试的技术水平。

申请我们的实习计划!

我们实习生的奉献精神和创新能力体现了Trail of Bits对推进网络安全和技术的承诺。与今年的夏季实习生团队合作非常愉快,我们迫不及待想看到他们未来的成就。

我们将在明年一月开放夏季实习生申请流程!

comments powered by Disqus
使用 Hugo 构建
主题 StackJimmy 设计