CT-T: Practical Formal Verification By Specification Extraction
CT-T:通过规范提取进行实用形式验证
基本信息
- 批准号:0716478
- 负责人:
- 金额:$ 80万
- 依托单位:
- 依托单位国家:美国
- 项目类别:Standard Grant
- 财政年份:2007
- 资助国家:美国
- 起止时间:2007-09-01 至 2012-08-31
- 项目状态:已结题
- 来源:
- 关键词:
项目摘要
Trust in a system can be compromised in many places. Extensive research has been conducted on the development of trustworthy requirements and policies, but those requirements and policies are effective only if they are carried out correctly. Ensuring the absence of implementation flaws by testing is inadequate; testing cannot be exhaustive and thus can miss critical vulnerabilities. Formal verification?proof that the system correctly implements its specification and enforces its policies?is an attractive alternative. Standard approaches to formal verification are powerful, but experience has shown them to challenging to use. Specification languages fail to describe complete systems, tools with limited capabilities cannot be integrated, verification techniques are difficult and time consuming to apply, and verification requires high levels of expertise. Current approaches also impose limitations on developers that make it difficult to fit formal verification into the development cycle.Our approach, Echo, is a new approach to formal software verification that makes such verification readily available, applicable, cost effective, and useful to the community that needs it. The basis of our approach, in stark contrast to traditional methods, is to transform the program, extract a high-level specification from a low-level one, and prove that it implies the original specification. The required analysis is split between a powerful general-purpose theorem-proving system and a low-level verification system.Echo will improve security and other facets of dependability in important computer applications thereby reducing losses resulting from security attacks and other failures.
对一个系统的信任在很多地方都会受到损害。人们对制定值得信赖的要求和政策进行了广泛的研究,但这些要求和政策只有在正确执行的情况下才有效。通过测试来确保没有实现缺陷是不够的;测试不可能是详尽的,因此可能会遗漏关键的漏洞。正式验证?证明系统正确地实现了其规范并执行了其策略?是一个有吸引力的选择。形式验证的标准方法是强大的,但经验表明,使用它们具有挑战性。规范语言无法描述完整的系统,功能有限的工具无法集成,验证技术难以应用且耗时,验证需要高水平的专业知识。当前的方法也对开发人员施加了限制,使得难以将形式化验证融入开发周期。我们的方法Echo是一种新的形式化软件验证方法,它使这种验证易于获得,适用,成本有效,并且对需要它的社区有用。与传统方法形成鲜明对比的是,我们方法的基础是将程序转换为可执行程序,从低级规范中提取高级规范,并证明它隐含原始规范。所需的分析分为一个强大的通用定理证明系统和一个低级验证系统。Echo将提高重要计算机应用程序的安全性和其他方面的可靠性,从而减少安全攻击和其他故障造成的损失。
项目成果
期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
数据更新时间:{{ journalArticles.updateTime }}
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
John Knight其他文献
The Rural-Urban Divide: Economic Disparities and Interactions in China . By John Knight and Lina Song. Oxford: Oxford University Press, 1999. xvii, 352 pp. $85.00 (cloth).
城乡差距:中国的经济差距和相互作用。
- DOI:
10.2307/2659518 - 发表时间:
2001 - 期刊:
- 影响因子:0
- 作者:
David Zweig;John Knight;Lina Song - 通讯作者:
Lina Song
MP12-01 INCREASED URINARY EXCRETION OF GLYCOLATE AND OXALATE IN OBESE AND DIABETIC MICE MODELS
- DOI:
10.1016/j.juro.2017.02.423 - 发表时间:
2017-04-01 - 期刊:
- 影响因子:
- 作者:
Kyle Wood;John Knight;Dean Assimos;Ross Holmes - 通讯作者:
Ross Holmes
1646: Variability of Oxalobacter Formigenes in Stool
- DOI:
10.1016/s0022-5347(18)31834-2 - 发表时间:
2007-04-01 - 期刊:
- 影响因子:
- 作者:
Sergey Prokopovich;John Knight;Ross P. Holmes;Dean G. Assimos - 通讯作者:
Dean G. Assimos
MP24-04 URINARY OXALATE EXCRETION IN OBESE MOUSE MODEL
- DOI:
10.1016/j.juro.2018.02.757 - 发表时间:
2018-04-01 - 期刊:
- 影响因子:
- 作者:
Kyle Wood;John Knight;Dean Assimos;Barbara Gower;Ross Holmes - 通讯作者:
Ross Holmes
China's growing but slowing inequality of household wealth, 2013–2018: A challenge to ‘common prosperity’?
2013 至 2018 年中国家庭财富不平等加剧但增速放缓:对“共同富裕”的挑战?
- DOI:
10.1016/j.chieco.2023.101947 - 发表时间:
2023-06-01 - 期刊:
- 影响因子:5.500
- 作者:
Haiyuan Wan;John Knight - 通讯作者:
John Knight
John Knight的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('John Knight', 18)}}的其他基金
SHF: Medium: Assurance Based Development: A Rational Approach To Creating High Assurance Software
SHF:中:基于保证的开发:创建高保证软件的合理方法
- 批准号:
0905375 - 财政年份:2009
- 资助金额:
$ 80万 - 项目类别:
Standard Grant
CSR: EHS: Assurance-Based Development of Critical Embedded Systems
CSR:EHS:关键嵌入式系统的基于保证的开发
- 批准号:
0720794 - 财政年份:2007
- 资助金额:
$ 80万 - 项目类别:
Standard Grant
CT-T: A System Structure for Secretless Security
CT-T:无秘密安全的系统结构
- 批准号:
0524432 - 财政年份:2005
- 资助金额:
$ 80万 - 项目类别:
Standard Grant
Next Generation Laboratories in Computer Science Education
下一代计算机科学教育实验室
- 批准号:
0127452 - 财政年份:2002
- 资助金额:
$ 80万 - 项目类别:
Standard Grant
ITR: Collaborative Research: Natural Language in the Development of High Confidence Software
ITR:协作研究:高可信度软件开发中的自然语言
- 批准号:
0205447 - 财政年份:2002
- 资助金额:
$ 80万 - 项目类别:
Continuing Grant
The Somerset Laboratory: An Open Facility for Experimentation in Safety-Critical Systems
萨默塞特实验室:安全关键系统实验的开放设施
- 批准号:
9525843 - 财政年份:1996
- 资助金额:
$ 80万 - 项目类别:
Standard Grant
A Case Study in Fault Tolerance and Software Safety
容错和软件安全案例研究
- 批准号:
9213427 - 财政年份:1992
- 资助金额:
$ 80万 - 项目类别:
Standard Grant
相似海外基金
Practical Framework for the Formal Verification of Cooperative Mobile Robots Algorithms
协作移动机器人算法形式化验证的实用框架
- 批准号:
21K11748 - 财政年份:2021
- 资助金额:
$ 80万 - 项目类别:
Grant-in-Aid for Scientific Research (C)
SHF: Small: Practical and Formal Foundations for Intermittent Computer Systems
SHF:小型:间歇计算机系统的实用和正式基础
- 批准号:
2007998 - 财政年份:2020
- 资助金额:
$ 80万 - 项目类别:
Standard Grant
Extracting information for correction of flaws from embedded system specification of practical scale by formal method
采用形式化方法从实用规模的嵌入式系统规范中提取缺陷修正信息
- 批准号:
24500032 - 财政年份:2012
- 资助金额:
$ 80万 - 项目类别:
Grant-in-Aid for Scientific Research (C)
Designing practical algorithms for learning formal languages based on distribution of strings in contexts
设计基于上下文中字符串分布的学习形式语言的实用算法
- 批准号:
23700156 - 财政年份:2011
- 资助金额:
$ 80万 - 项目类别:
Grant-in-Aid for Young Scientists (B)
Practical advances in the formal verification of security and safety critical software
安全和安全关键软件形式化验证的实际进展
- 批准号:
261573-2008 - 财政年份:2011
- 资助金额:
$ 80万 - 项目类别:
Discovery Grants Program - Individual
Practical advances in the formal verification of security and safety critical software
安全和安全关键软件形式化验证的实际进展
- 批准号:
261573-2008 - 财政年份:2010
- 资助金额:
$ 80万 - 项目类别:
Discovery Grants Program - Individual
Formal verification of practical game narratives
实际游戏叙述的形式化验证
- 批准号:
398393-2010 - 财政年份:2010
- 资助金额:
$ 80万 - 项目类别:
University Undergraduate Student Research Awards
Practical advances in the formal verification of security and safety critical software
安全和安全关键软件形式化验证的实际进展
- 批准号:
261573-2008 - 财政年份:2009
- 资助金额:
$ 80万 - 项目类别:
Discovery Grants Program - Individual
Study on Formal Methods Applicable to Practical Software Development
适用于实际软件开发的形式化方法研究
- 批准号:
21300009 - 财政年份:2009
- 资助金额:
$ 80万 - 项目类别:
Grant-in-Aid for Scientific Research (B)
Practical methods and tools for the formal analysis of software artifacts
软件工件形式化分析的实用方法和工具
- 批准号:
228103-2004 - 财政年份:2008
- 资助金额:
$ 80万 - 项目类别:
Discovery Grants Program - Individual