检索结果-南通市图书馆

formal verification of Data Modifications in Cloud Block Storage Based on Separation Logic

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Chinese Journal of Electronics 2024年第1期33卷 112-127页

作者： Bowen ZHANG Zhao JIN Hanpin WANG Yongzhi CAO Key Laboratory of High Confidence Software Technologies (MOE) School of Computer Science Peking University School of Computer and Artificial Intelligence Zhengzhou University School of Computer Science and Cyber Engineering Guangzhou University

Cloud storage is now widely used, but its reliability has always been a major concern. Cloud block storage(CBS) is a famous type of cloud storage. It has the closest architecture to the underlying storage and can provide interfaces for other types. Data modifications in CBS have potential risks such as null reference or data *** verification of these operations can improve the reliability of CBS to some extent. Although separation logic is a mainstream approach to verifying program correctness, the complex architecture of CBS creates some challenges for verifications. This paper develops a proof system based on separation logic for verifying the CBS data modifications. The proof system can represent the CBS architecture, describe the properties of the CBS system state, and specify the behavior of CBS data modifications. Using the interactive verification approach from Coq, the proof system is implemented as a verification tool. With this tool, the paper builds machine-checked proofs for the functional correctness of CBS data modifications. This work can thus analyze the reliability of cloud storage from a formal perspective.

关键词： Cloud computing Behavioral sciences Reliability formal verification

同方期刊数据库

formal verification Platform as a Service:WebAssembly Vulnerability Detection Application

在线全文

学校读者我要写书评

暂无评论

Computer Systems Science & Engineering 2023年第5期45卷 2155-2170页

作者： LiangJun Deng Hang Lei Zheng Yang WeiZhong Qian XiaoYu Li Hao Wu Sihao Deng RuChao Sha WeiDong Deng School of Information and Software Engineering University of Electronic Science and Technology of ChinaChengdu610054China School of Physics University of Electronic Science and Technology of ChinaChengdu611731China ICB-PMDM-LERMPS UMR 6303 CNRSUTBMUniversitéde Bourgogne Franche-ComtéBelfort90010France Chengdu Railway Science and Technology Innovation Co.LTD Chengdu640041China

In order to realize a general-purpose automatic formal verification platform based on WebAssembly technology as a web service(FVPS),which aims to provide an automated report of vulnerability detections,this work builds a Hyperledger Fabric blockchain runtime *** proposes an optimized methodology of the functional equivalent translation from source program languages to formal *** methodology utilizes an external application programming interface(API)table to replace the source codes in compilation,thereby pruning the part of housekeeping codes to ease code *** inflation is a significant metric in formal language ***,minor code inflation enhances verification scale and performance *** determines the efficiency of formal verification,involving launching,running,and memory *** instance,path explosion increases exponentially,resulting in *** experimental results conclude that program languages like golang severely impact code *** reduces the wasm code size by over 90%,achieving two orders of optimization magnitude,from 2000 kilobyte(KB)to 90 *** means we can cope with golang applications up to 20 times larger than the original in *** work eliminates the gap between Hyperledger Fabric smart contracts and *** approach is pragmatic,adaptable,extendable,and ***,FVPS is successfully applied in a Railway-Port-Aviation blockchain transportation system.

关键词： WebAssembly formal verification blockchain smart contract

formal verification of synchronous data-flow program transformations toward certified compilers

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2013年第5期7卷 598-616页

作者： Van Chan NGO Jean-Pierre TALPIN Thierry GAUTIER Paul Le GUERNIC Loic BESNARD INRIA Rennes-Bretagne Atlantique Rennes 35042 France IRISA/CNRS Rennes 35042 France

Translation validation was invented in the 90＇s by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translation validators attempt to verify that program transformations preserve semantics. In this work, we adopt this approach to formally verify that the clock semantics and data dependence are preserved during the compilation of the Signal compiler. Translation valida- tion is implemented for every compilation phase from the initial phase until the latest phase where the executable code is generated, by proving the transformation in each phase of the compiler preserves the semantics. We represent the clock semantics, the data dependence of a program and its trans- formed counterpart as first-order formulas which are called clock models and synchronous dependence graphs （SDGs）, respectively. We then introduce clock refinement and depen- dence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock mod- els and SDGs, respectively. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.

关键词： formal verification translation validation certi-fied compiler multi-clocked synchronous programs embed-ded systems.

formal verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2011年第6期26卷 1017-1030页

作者：曹军威张帆许可刘连臣吴澄 CCF ACM IEEE Research Institute of Information Technology Tsinghua University Tsinghua National Laboratory for Information Science and Technology National CIMS Engineering and Research Center Tsinghua University Morgan Stanley

With quick development of grid techniques and growing complexity of grid applications, it is becoming critical for reasoning temporal properties of grid workflows to probe potential pitfalls and errors, in order to ensure reliability and trustworthiness at the initial design phase. A state Pi calculus is proposed and implemented in this work, which not only enables fexible abstraction and management of historical grid verification of grid workflows. Furthermore, a relaxed region system events, but also facilitates modeling and temporal analysis （RRA） approach is proposed to decompose large scale grid workflows into sequentially composed regions with relaxation of parallel workflow branches, and corresponding verification strategies are also decomposed following modular verification principles. Performance evaluation results show that the RRA approach can dramatically reduce CPU time and memory usage of formal verification.

关键词： grid computing workflow management formal verification state Pi calculus

维普期刊数据库

formal verification of TASM Models by Translating into UPPAAL

在线全文

学校读者我要写书评

暂无评论

Journal of Donghua University(English Edition) 2012年第1期29卷 51-54页

作者：胡凯张腾杨志斌顾斌蒋树姜泮昌 School of Computer Science and Engineering Beihang University Beijing Institute of Control Engineering

Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. formal verification of TASM model can be fulfilled through model checking activities by translating into UPPAAL. Firstly, the translational semantics from TASM to UPPAAL is presented through atlas transformation language(ATL). Secondly, the implementation of the proposed model transformation tool TASM2UPPAAL is provided. Finally, a case study is given to illustrate the automatic transformation from TASM model to UPPAAL model.

关键词： timed abstract state machine(TASM) formal verification model transformation atlas transformation language(ATL) UPPAAL

维普期刊数据库

formal verification under Unknown Constraints

在线全文

学校读者我要写书评

暂无评论

Wuhan University Journal of Natural Sciences 2005年第1期10卷 43-46页

作者： LI Guang-hui 1,2,3 , LI Xiao-wei 2,31. School of Information Engineering, Zhejiang Forestry College, Hangzhou 311300, Zhejiang, China 2. Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100080, China 3. Graduate School of the Chinese Academy of Sciences, Beijing 100039, China School of Information Engineering Zhejiang Forestry College Hangzhou Zhejiang China Institute of Computing Technology Chinese Academy of Sciences Beijing China Graduate School of the Chinese Academy of Sciences Beijing China

We present a formal method of verifying designs with unknown constraints (e.g., black boxes) using Boolean satisfiability (SAT). This method is based on a new encoding scheme of unknown constraints, and solves the corresponding conjunctive normal form (CNF) ***,this method can avoid the potential memory explosion, which the binary decision diagram (BDD) based techniques maybe suffer from, thus it has the capacity of verifying large designs. Experimental results demonstrate the efficiency and feasibility of the proposed method.

关键词： formal verification unknown constraints black box Boolean satisfiability Boolean comparison

维普期刊数据库

Design and formal verification of a CEM protoco with transparent TTP

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2013年第2期7卷 279-297页

作者： Zhiyuan LIU Jun PANG Chenyi ZHANG School of Management Science and Engineering Shandong Normal UniversityChina Jinan 250000 Faculty of Science Technology and Communication University of LuxembourgLuxembourg Luxembourg 1359 School of Information Technology and Electrical Engineering University of Queensland Australia Brisbane QLD4072

In certified email （CEM） protocols, trusted third party （TTP） transparency is an important security require- ment which helps to avoid bad publicity as well as protecting individual users＇ privacy. Cederquist et al. proposed an opti- mistic certified email protocol, which employs key chains to reduce the storage requirement of the TTE We extend their protocol to satisfy the property of TTP transparency, using existing verifiably encrypted signature schemes. An imple- mentation with the scheme based on bilinear pairing makes our extension one of the most efficient CEM protocols satis- fying strong fairness, timeliness, and TTP transparency. We formally verify the security requirements of the extended pro- tocol. The properties of fairness, timeliness and effectiveness are checked in the model checker Mocha, and TTP trans- parency is formalised and analysed using the toolsets/~CRL and CADE

关键词： fair exchange CEM protocols fairness TTPtransparency formal verification

Research on Microkernel Integrity Semantics Model and formal verification

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Chinese Journal of Electronics 2014年第1期23卷 43-48页

作者： QIAN Zhenjiang LIU Wei HUANG Hao State Key Laboratory for Novel Software Technology Nanjing University Department of Computer Science and Technology Nanjing University

Microkernel integrity is an important aspect of security for the whole microkernel system. Many of the research works on microkernel integrity focus on analysis and safeguards against the existing kernel attacks, and security enhancements for the vulnerabilities of system design and implementation aspects. The formal methods for operating system design and verification ensure the system’s high level of security. The existing formalization work and research for operating system mainly focus on the code-level verification of program correctness. In this paper, we propose a formal abstraction model of microkernel in order to accurately describe the semantics of every kernel behavior, and achieve the description of the whole kernel. Based on the model we illustrate the microkernel integrity criterions and elaborate on the integrity mechanism. Meanwhile, we formally verify the completeness and consistency between the mechanism and the definition of the microkernel integrity. We use the self-implemented operating system VTOS(Verified trusted operating system) as an example to illustrate the design method for the microkernel integrity.

关键词： Microkernel integrity Integrity mechanism Integrity semantics model formal verification

Cloud Manufacturing Service Composition Modeling and formal verification Based on Calculus for Orchestration of Web Service

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Cloud Manufacturing Service Composition Modeling and Formal ...