What exactly does "stack safety" mean? The phrase is associated with a variety of compiler, run-time, and hardware mechanisms for protecting stack memory. But these mechanisms typically lack precise specifications, relying instead on informal descriptions and examples of bad behaviors that they prevent. We propose a formal characterization of stack safety, formulated with concepts from language-based security: a combination of an integrity property ("the private state in each caller's stack frame is held invariant by the callee"), a confidentiality property ("the callee's behavior is insensitive to the caller's private state"), and a well-bracketedness property ("each callee returns control to its immediate caller"). We use these properties to validate the stack-safety "micro-policies" proposed by Roessler and DeHon [2018]. Specifically, we check (with property-based random testing) that Roessler and Dehon's "eager" micro-policy, which catches violations as early as possible, enforces a simple "stepwise" variant of our properties and correctly detects several broken variants, and that (a repaired version of) their more performant "lazy" micro-policy corresponds to a slightly weaker and more extensional "observational" variant of our properties.


翻译:“ 堆叠安全” 的确切含义是什么? 短语是指各种编译者、 运行时间和硬件机制来保护堆叠内存。 但这些机制通常缺乏精确的规格, 通常依赖非正式描述和他们防止的不良行为实例。 我们提议对堆叠安全进行正式定性, 其设计概念来自基于语言的安全: 完整财产( “ 每个调用者堆叠框中的私人状态” ) 、 保密财产( “ 被调用者的行为对调用者的私人状态不敏感 ” ), 以及一个井井然有序的财产( “ 每一个被调用者将控制归到其直接的调用者 ” ) 。 我们使用这些属性来验证罗斯勒和德洪[ 2018] 提出的堆叠安全“ 宏观政策” 。 具体地说, 我们检查( 以地产为基础的随机测试), Roessler 和 Dehon的“ eger” 微观政策( ), 尽可能早地捕捉到违规情况, 执行简单的“ ” 变式的“ ”, 正确探测到几个变式的变式, 的变式“ 和变式“ 的“ 较弱的变式” 。

0
下载
关闭预览

相关内容

《计算机信息》杂志发表高质量的论文,扩大了运筹学和计算的范围,寻求有关理论、方法、实验、系统和应用方面的原创研究论文、新颖的调查和教程论文,以及描述新的和有用的软件工具的论文。官网链接:https://pubsonline.informs.org/journal/ijoc
霍普金斯《操作系统原理》2020课程,不可错过!
专知会员服务
36+阅读 · 2020年10月27日
专知会员服务
39+阅读 · 2020年9月6日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
机器学习相关资源(框架、库、软件)大列表
专知会员服务
39+阅读 · 2019年10月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
计算机 | 中低难度国际会议信息6条
Call4Papers
7+阅读 · 2019年5月16日
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
动物脑的好奇心和强化学习的好奇心
CreateAMind
10+阅读 · 2019年1月26日
spinningup.openai 强化学习资源完整
CreateAMind
6+阅读 · 2018年12月17日
已删除
将门创投
5+阅读 · 2018年6月7日
强化学习族谱
CreateAMind
26+阅读 · 2017年8月2日
Arxiv
12+阅读 · 2020年12月10日
Self-Driving Cars: A Survey
Arxiv
41+阅读 · 2019年1月14日
VIP会员
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
计算机 | 中低难度国际会议信息6条
Call4Papers
7+阅读 · 2019年5月16日
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
动物脑的好奇心和强化学习的好奇心
CreateAMind
10+阅读 · 2019年1月26日
spinningup.openai 强化学习资源完整
CreateAMind
6+阅读 · 2018年12月17日
已删除
将门创投
5+阅读 · 2018年6月7日
强化学习族谱
CreateAMind
26+阅读 · 2017年8月2日
Top
微信扫码咨询专知VIP会员