Lessons Learned in Game Development for Crowdsourced Software Formal Verification
Lessons Learned in Game Development for Crowdsourced Software Formal Verification
复制标题
众包软件形式验证游戏开发中的经验教训
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
T. Maddern
中科院分区：
文献类型：
--
作者：
Drew Dean;Sean Gaurino;Leonard Eusebi;A. Keplinger;Christopher Ganas;Timothy Pavlik;Ronald J. Watro;Aaron Cammarata;John T. Murray;Kelly McLaughlin;J. Cheng;T. Maddern
引言形式方法和计算机安全研究的历史源远流长，交织在一起。在理论上能够证明软件安全属性的程序逻辑是在20世纪70年代早期开发出来的[1]。第一批安全模型的开发[2-4]引发了一种愿望，即证明这些模型实际上确实执行了它们声称的属性，并且该模型的实际实现相对于其规范是正确的[5；6]。乐观主义在20世纪80年代初至中期达到顶峰[7-11]，正式安全方法的顶峰在《橙色书》出版前不久达到[12]，其中A1类系统的认证需要正式方法。软件的正式验证被认为是软件强制执行特定属性集的黄金标准证据。不久之后，正式方法在时间和金钱上的成本变得非常明显。主流计算机安全研究将重点转移到密码协议(例如[13；14])的分析上，围绕密码密钥管理的策略[15]，以及对当代系统中发现的安全问题的巧妙修复[16-19]。
Introduction The history of formal methods and computer security research is long and intertwined. Program logics that were in theory capable of proving security properties of software were developed by the early 1970s [1]. The development of the first security models [2-4] gave rise to a desire to prove that the models did, in fact, enforce the properties that they claimed to, and that an actual implementation of the model was correct with respect to its specification [5; 6]. Optimism reached its peak in the early to mid-1980s [7-11], and the peak of formal methods for security was reached shortly before the publication of the Orange Book [12], where the certification of a system at class A1 required formal methods. Formal verification of software was considered the gold standard evidence that the software enforced a particular set of properties. Soon afterwards, the costs of formal methods, in both time and money, became all too apparent. Mainstream computer security research shifted focus to analysis of cryptographic protocols (e.g. [13; 14]), policies around cryptographic key management [15], and clever fixes for security problems found in contemporary systems [16-19].