paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Typed and Confused: Studying the Unexpected Dangers of Gradual Typing

类型化与困惑:研究渐进类型(gradual typing)的意外危险
ASE Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering2024匹配度 3/10 · 论文属于程序语言与静态分析/类型系统领域,关注渐进类型与类型混淆,但未涉及 LLM/Agent、机器学习系统、浮点程序分析或贝叶斯程序分析,与用户当前核心交叉方向关联较弱。引用 4 inbox
Dominic Troppmann, Aurore Fass, Cristian-Alexandru Staicu
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:通过 3 万个开源仓库的实证研究,揭示渐进类型标注可能误导开发者、削弱运行时检查并引发类型混淆。

脚本语言因动态弱类型而灵活,却难捕获细微缺陷;TypeScript 等渐进类型系统允许可选类型标注,但许多部署仅做静态检查,不在运行时强制类型提示。开发者必须在已标注与未标注代码边界手写显式检查,遗漏会造成类型不一致,涉及用户输入时更导致类型混淆。本文对 30,000 个开源仓库做大规模实证研究,静态分析渐进类型使用及其对显式检查的影响。结果显示,许多项目虽含渐进类型代码但仅占小部分,存在大量需要显式检查的过渡点;原始类型参数标注可能产生退化效应。人工分析还表明,攻击者可远程触发类型混淆并违反类型提示。

问题
动态脚本语言的渐进类型系统常仅做静态检查而不在运行时强制类型提示,导致开发者在类型边界缺少显式检查;本文研究这种不健全性是否会导致类型不一致与类型混淆漏洞。
方法
对 30,000 个开源仓库进行大规模静态实证分析,度量渐进类型(可选标注)的使用范围及其与显式运行时类型检查的关系,并人工分析部分仓库验证可利用性。
评估
通过仓库级统计与人工分析发现:渐进类型代码普遍存在但占比小,产生大量过渡点;原始类型参数标注可能恶化显式检查;攻击者可远程触发类型混淆并违反类型提示。
原文摘要(Abstract)

In recent years, scripting languages such as JavaScript and Python have gained a lot of traction due to their flexibility, which allows developers to write concise code in a short amount of time. However, this flexibility is achieved via weak, dynamic typing, which fails to catch subtle bugs that would be prevented by a compiler, in static typing. Gradual-type systems like TypeScript emerged as a solution that combines the best of both worlds, allowing developers to annotate parts of their code with optional type hints. Nonetheless, most practical deployments of such systems are unsound, limiting themselves to static checks and not performing residual runtime checks that help enforce type hints uniformly. This is a missed automation opportunity that offloads the burden on developers, who still need to perform explicit type checks at transition points between untyped and typed code so that values at runtime obey the type hints. Failure to do so can result in subtle type inconsistency bugs, and when user input is involved, it can render input validation mechanisms ineffective, resulting in type confusion problems. In this work, we study the relation between gradual typing and type confusion. Our main hypothesis is that the type hints in the code can mislead developers into thinking they are enforced consistently by the compiler, resulting in a lack of explicit runtime checks that ensure type safety. We perform a large empirical study with 30,000 open-source repositories to statically analyze if and how they use gradual typing and to what extent this influences the presence of explicit type checks. We find that many projects feature gradually typed code, but usually only in small portions of their code base. This implies the presence of many points in the code base where developers must add explicit type checks, i.e., at the transition points between unannotated and annotated code. Our results further indicate that gradual typing may have a deteriorating effect when parameters are annotated with primitive types. Finally, we manually analyze a small portion of the studied repositories and show that attackers can remotely cause type confusion and violate the type hints added by developers. We hope that our results help raise awareness about the limits of current gradual-type systems and their unwanted effect on input validation.

链接与引用

DOI 原文 · DBLP

BibTeX
@inproceedings{TroppmannFS24,
  title = {Typed and Confused: Studying the Unexpected Dangers of Gradual Typing},
  author = {Dominic Troppmann and Aurore Fass and Cristian-Alexandru Staicu},
  booktitle = {ASE},
  year = {2024},
  doi = {10.1145/3691620.3695549}
}