Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)

机译：使用ITPS的软件验证应使用二进制代码提取以减少TCB（短文）

获取原文

页面导航

摘要
著录项
相似文献
相关主题

摘要

LCF-style provers emphasise that all results are secured by logical inference, and yet their current facilities for code extraction or code generation fall short of this high standard. This paper argues that extraction mechanisms with a small trusted computing base (TCB) ought to be used instead, pointing out that the recent CakeML and CEuf projects show that this is possible in HOL and within reach in Coq.

机译：LCF样式的普通强调所有结果都是通过逻辑推理获得的，但他们目前的代码提取或代码生成设施缺少这一高标准。本文认为，具有小值得信赖的计算基础（TCB）的提取机制应该被使用，指出最近的Cakeml和CEUF项目表明，在HOL和COQ中的范围内，这是可能的。

著录项

来源
《International Conference on Interactive Theorem Proving》|2018年|642p|共8页
会议地点
作者
Ramana Kumar; Eric Mullen; Zachary Tatlock; Magnus O. Myreen;
展开▼
作者单位

展开▼
会议组织
原文格式 PDF
正文语种
中图分类 TP301-53;
关键词

相似文献

外文文献
中文文献
专利

1. Low-Power Code Memory Integrity Verification Using Background Cyclic Redundancy Check Calculator Based on Binary Code Inversion Method [J] . Park Daejin Journal of circuits, systems and computers . 2016,第7期

机译：基于二进制代码反演方法的背景循环冗余校验计算器进行低功耗代码存储器完整性验证
2. Embedded software verification in hardware-software codesign [J] . Pao-Ann Hsiung Journal of systems architecture . 2000,第15期

机译：硬件-软件代码签名中的嵌入式软件验证
3. Lossy Coding of Binary Sources with Short Linear Codes [J] . Misako KOTANI, Motohiko ISAKA IEICE Transactions on fundamentals of electronics, communications & computer sciences . 2010,第11期

机译：短线性码二进制源的有损编码
4. Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper) [C] . Ramana Kumar, Eric Mullen, Zachary Tatlock, Interactive theorem proving . 2018

机译：使用ITP进行软件验证应使用二进制代码提取来减少TCB（简短论文）
5. Reduced-complexity VLSI architectures for binary and nonbinary LDPC codes. [D] . Kim, Sangmin. 2010

机译：降低复杂度的VLSI架构，用于二进制和非二进制LDPC码。
6. Automated concept-level information extraction to reduce the need for custom software and rules development [O] . Leonard W DAvolio, Thien M Nguyen, Sergey Goryachev, 2011

机译：自动化的概念层信息提取减少了对定制软件和规则开发的需求
7. Pyramidal groups, in Italy and elsewhere, represent a model of separation of ownership and control. Pyramids typically have blockholders which extract private benefits of control at the expenses of minority shareholder. This paper focuses on the Italian case where the number of pyramids is reducing but are still largely diffused. Groups are a form of entrenchment and may have negative effects on firm growth. They are characterized by conflicts of interest and self-dealing practices which reduced external financing opportunities. In this paper legal regulation of groups in Italy is discussed, which has positive aspects (art. 2497 ss. c.c.) but some weaknesses on self-dealing practices (artt. 2391 and 2391-bis c.c.). Future reforms should take into consideration the guidelines given at European level (for instance, by the High Level Group of Company Law Experts and the European Commission), which have been set aside from the political agendas of mostly European governments. Moreover, we suggest to strengthen the process of (not only formal) disclosure of relevant information to the company shareholders’ as well, in order not to dismantle pyramids, but to make them “shorter” (when that is the case), more transparent and reciprocally competitive. [O] . Giacomo Bosi, Sandro Trento 100

机译：在意大利和其他地方的金字塔群体代表了所有权和控制权分离的模式。金字塔通常拥有大股东，以小股东的利益为代价提取控制权的私人利益。本文重点关注意大利案例，其中金字塔的数量在减少，但仍然在很大程度上分散。群体是一种壕沟形式，可能对企业的成长产生负面影响。它们的特点是利益冲突和自我交易做法，减少了外部融资机会。在本文中，讨论了意大利群体的法律规定，它具有积极的方面（第2497条，c.c。），但在自我交易实践方面存在一些弱点（第2391条和第2391条之二）。未来的改革应该考虑到欧洲层面的指导方针（例如，公司法专家和欧洲委员会的高级别小组），这些指导方针已被搁置在主要是欧洲政府的政治议程之外。此外，我们建议加强（不仅正式）向公司股东披露相关信息的过程，以便不拆除金字塔，而是使它们“更短”（在这种情况下），更透明并且相互竞争。

Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)

摘要

著录项

相似文献

相关主题

期刊订阅