• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Interactive theorem proving >Program Verification in the Presence of Cached Address Translation
【24h】

Program Verification in the Presence of Cached Address Translation

机译：存在缓存地址转换的程序验证

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Operating system (OS) kernels achieve isolation between user-level processes using multi-level page tables and translation looka-side buffers (TLBs). Controlling the TLB correctly is a fundamental security property-yet all large-scale formal OS verification projects leave correct functionality of the TLB as an assumption. We present a logic for reasoning about low-level programs in the presence of TLB address translation. We extract invariants and necessary conditions for correct TLB operation that mirror the informal reasoning of OS engineers. Our program logic reduces to a standard logic for user-level reasoning, reduces to side-condition checks for kernel-level reasoning, and can handle typical OS kernel tasks such as context switching and page table manipulations.
机译：操作系统（OS）内核使用多级页表和转换后备缓冲区（TLB）在用户级进程之间实现隔离。正确控制TLB是一项基本的安全属性，但所有大型正式OS验证项目都将TLB的正确功能作为假设。我们提出了一种在存在TLB地址转换的情况下对底层程序进行推理的逻辑。我们提取不变量和正确的TLB操作所需的必要条件，以反映OS工程师的非正式推理。我们的程序逻辑简化为用于用户级推理的标准逻辑，简化为内核级推理的附带条件检查，并且可以处理典型的OS内核任务，例如上下文切换和页表操作。

著录项

  • 来源
    《Interactive theorem proving》|2018年|542-559|共18页
  • 会议地点 Oxford(GB)
  • 作者

    Hira Taqdees Syeda; Gerwin Klein;

  • 作者单位

    Data61, CSIRO, Eveleigh, Australia,School of Computer Science and Engineering, UNSW, Sydney, Australia;

    Data61, CSIRO, Eveleigh, Australia,School of Computer Science and Engineering, UNSW, Sydney, Australia;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号