POSIX file store in Z/Eves: An experiment in the verified software repository

We present results from the second pilot project in the international Verification Grand Challenge: a formally verified specification of a POSIX-compliant file store using the Z/Eves theorem prover. The project’s overall objective is to build a verified file store for space-flight missions. Our specification of the file store is based on Morgan and Sufrin’s specification of the UNIX filing system; the proof and its mechanisation in Z/Eves are novel. We show how our work contributes towards building a verified software repository: a set of general theories, proof techniques, and experiments reusable across different domains.     

Mechanising Mondex with Z/Eves

We describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach and mechanised the original LaT_EX sources without changing their technical content, except to correct errors. We found problems in the original specification and some missing invariants in the refinements. Based on these experiences, we present novel and detailed guidance on how to drive Z/Eves successfully. The work contributes to the Repository for the Verified Software Grand Challenge. C. B. Jones     

Verification of clock synchronization algorithms: experiments on a combination of deductive tools

We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider’s generalized clock synchronization protocol [Sch87] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius–Lynch [LL84], satisfy Schneider’s general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetics.     

Inductive assertions and operational semantics

This paper shows how classic inductive assertions can be used in conjunction with a formal operational semantics to prove partial correctness properties of programs. The method imposes only the proof obligations that would be produced by a verification condition generator – but does not require the definition of a verification condition generator. All that is required is a theorem prover, a formal operational semantics, and the object program with appropriate assertions at user-selected cut points. The verification conditions are generated in the course of the theorem-proving process by straightforward symbolic evaluation of the formal operational semantics. The technique is demonstrated by proving the partial correctness of simple bytecode programs with respect to a preexisting operational model of the Java Virtual Machine.     

电子商务中安全协议的验证方法

该文简述了电子商务中的安全协议验证技术,对目前的一些重要的研究方法进行了分析和比较,重点针对形式化的方法在电子商务中的安全协议验证中的优势和不足,结合实际,提出了一些可能的发展趋势。     

A sequent-style model elimination strategy and a positive refinement

We present a sequent style proof system related to the MESON procedure, which is itself based on the model elimination strategy for mechanical theorem proving. The MESON procedure is attractive because it is a problem reduction format, that is, it has a goal-subgoal structure. The sequent style system based on it shares this advantage, and also has a simple declarative semantics and soundness proof. A refinement of the sequent style system tends to produce shorter sequents and may facilitate the use of the MESON procedure with caching of solutions to subgoals to avoid repeated work on the same subgoal. In the MESON procedure, a goal is marked contradicted and considered to be solved, if an ancestor goal is complementary to it. In the positive refinement, only the positive goals need to be checked for contradiction in this way. This means that if a list of ancestor goals is kept with each goal, it is only necessary to store the negative ancestor goals, since these are the only ones that need to be examined in testing if a positive goal is contradicted. Similar restrictions on the reduction operation of model elimination are possible.This research was supported in part by the National Science Foundation under grant DCR-8516243.     

An approach to formal verification of human–computer interaction

The correct functioning of interactive computer systems depends on both the faultless operation of the device and correct human actions. In this paper, we focus on system malfunctions due to human actions. We present abstract principles that generate cognitively plausible human behaviour. These principles are then formalised in a higher-order logic as a generic, and so retargetable, cognitive architecture, based on results from cognitive psychology. We instantiate the generic cognitive architecture to obtain specific user models. These are then used in a series of case studies on the formal verification of simple interactive systems. By doing this, we demonstrate that our verification methodology can detect a variety of realistic, potentially erroneous actions, which emerge from the combination of a poorly designed device and cognitively plausible human behaviour.     

State-of-the-art flash memory devices and post-flash emerging memories

Although conventional Floating gate (FG) flash memory has recently gone into the 2X nm node, the technology challenges are formidable below 20 nm. Charge-trapping (CT) devices are promising to scale beyond 20 nm but below 10 nm both CT and FG devices hold too few electrons for robust MLC (multi-level cell, or more than one bit storage per cell) storage. However, due to the simpler structure and its more robust storage (not sensitive to tunnel oxide defects since charges are stored in deep trap levels), CT i...     

Garbage collection of multi-version indexed data on flash memory

Maintaining a multi-version index on flash memory could generate a lot of updates and invalid pages. It is important to have an efficient garbage collection mechanism to ensure the flash memory has sufficient number of free blocks for storing new data versions and their index structures. In this paper, we study the important performance issues in using the purging-range query to reclaim the blocks, which are storing old data versions and invalid index entries, to be free blocks. To reduce the cost for processing the purging-range query, we propose the physical block labeling (PBL) scheme to provide a better estimation on the purging version number to be used for purging old data versions. To further enhance the performance of the garbage collection process, and at the same time to maximize the deadspans of data versions and balance the wear levels of the blocks, we propose two schemes called, the sequential placement (SQ) and frequency-based placement (FBP), for placing new data versions into free pages. As illustrated in the performance studies, both SQ and FBP can effectively balance the wear levels of the blocks. The deadspans of data versions are longer under FBP than both SQ and RR, and the page reallocation cost is also lower under FBP especially when the size of flash memory allocated for the database is limited. The experimental results also illustrate that PBL can effectively minimize the number of invocations of the purging-range query to be one to reclaim the required number of blocks in each garbage collection.     

A hybrid flash translation layer design for SLC-MLC flash memory based multibank solid state disk

This paper presents the design of a NAND flash based solid state disk (SSD), which can support various storage access patterns commonly observed in a PC environment. It is based on a hybrid model of high-performance SLC (single-level cell) NAND and low cost MLC (multi-level cell) NAND flash memories. Typically, SLC NAND has a higher transfer rate and greater cell endurance than MLC NAND flash memory. MLC NAND, on the other hand, benefits from lower price and higher capacity. In order to achieve higher performance than traditional SSDs, an interleaving technique that places NAND flash chips in parallel is essential. However, using the traditional FTL (flash translation layer) on an SSD with only MLC NAND chips is inefficient because the size of a logical block becomes large as the mapping address unit grows. In this paper, we proposed a HFTL (hybrid flash translation layer) which makes use of chained-blocks, combining SLC NAND and MLC NAND flash memories in parallel. Experimental results show that for most of the traces studied, the HFTL in an SSD configuration composed of 80% MLC NAND and 20% SLC NAND memories can improve performance compared to other solid state disk configurations, composed of either SLC NAND or MLC NAND flash memory alone.     

State-rich model checking

In this paper we survey the area of formal verification techniques, with emphasis on model checking due to its wide acceptance by both academia and industry. The major approaches and their characteristics are presented, together with the main problems faced while trying to apply them. With the increased complexity of systems, as well as interest in software correctness, the demand for more powerful automatic techniques is pushing the theories and tools towards integration. We discuss the state of the art in combining formal methods tools, mainly model checking with theorem proving and abstract interpretation. In particular, we present our own recent contribution on an approach to integrate model checking and theorem proving to handle state-rich systems specified using a combination of Z and CSP.     

Fine-grained updates in database management systems for flash memory

The growing storage capacity of flash memory (up to 640 GB) and the proliferation of small mobile devices such as PDAs and mobile phones makes it attractive to build database management systems (DBMSs) on top of flash memory. However, most existing DBMSs are designed to run on hard disk drives. The unique characteristics of flash memory make the direct application of these existing DBMSs to flash memory very energy inefficient and slow. The relatively few DBMSs that are designed for flash suffer from two major short-comings. First, they do not take full advantage of the fact that updates to tuples usually only involve a small percentage of the attributes. A tuple refers to a row of a table in a database. Second, they do not cater for the asymmetry of write versus read costs of flash memory when designing the buffer replacement algorithm. In this paper, we have developed algorithms that address both of these short-comings. We overcome the first short-coming by partitioning tables into columns and then group the columns based on which columns are read or updated together. To this end, we developed an algorithm that uses a cost-based approach, which produces optimal column groupings for a given workload. We also propose a heuristic solution to the partitioning problem. The second short-coming is overcome by the design of the buffer replacement algorithm that automatically determines which page to evict from buffer based on a cost model that minimizes the expected read and write energy usage. Experiments using the TPC-C benchmark [S.T. Leutenegger, D. Dias, A modeling study of the TPC-C benchmark, in: Proceedings of ACM SIGMOD, 1993, pp. 22-31] show that our approach produces up to 40-fold in energy usage savings compared to the state-of-the-art in-page logging approach.     

重写对策在基于HOL的形式化证明中的应用

讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用.通过REWRITE_ TAC对策、ASM_ REWRITE_ TAC对策和RW_ TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match搜索和DB.find搜索等重写对策的定理参数的选择方法,并进行了分析与比较.进一步说明了重写对策在基于HOL系统的形式化证明中的重要性,以期对HOL系统用户提供一些帮助与启发,促进HOL系统的进一步发展与完善,使形式化方法能够解决更多的实际问题.     

PORCE: An efficient power off recovery scheme for flash memory

Flash memory is now replacing hard disk in many embedded applications including cellular phones, digital cameras, car navigation systems, and so on. However, because flash memory has its own characteristics such as “erase-before-write” and wear-leveling, a software layer called FTL (flash translation layer) should be provided. However, most FTL algorithms did not include the power off recovery module though it is very important in portable devices. In this paper, we suggest an efficient power off recovery scheme for flash memory called PORCE (Power Off Recovery sChEme for flash memory). PORCE is tightly coupled to FTL operations and minimizes performance degradation during normal operations by storing recovery information as small as possible. Additionally, PORCE provides cost-based reclamation protocols which include the wear-leveling module. Our empirical study shows that PORCE is an efficient recovery protocol.     

Data loss recovery for power failure in flash memory storage systems

Due to the rapid development of flash memory technology, NAND flash has been widely used as a storage device in portable embedded systems, personal computers, and enterprise systems. However, flash memory is prone to performance degradation due to the long latency in flash program operations and flash erasure operations. One common technique for hiding long program latency is to use a temporal buffer to hold write data. Although DRAM is often used to implement the buffer because of its high performance and low bit cost, it is volatile; thus, that the data may be lost on power failure in the storage system. As a solution to this issue, recent operating systems frequently issue flush commands to force storage devices to permanently move data from the buffer into the non-volatile area. However, the excessive use of flush commands may worsen the write performance of the storage systems. In this paper, we propose two data loss recovery techniques that require fewer write operations to flash memory. These techniques remove unnecessary flash writes by storing storage metadata along with user data simultaneously by utilizing the spare area associated with each data page.     

A B-Tree index extension to enhance response time and the life cycle of flash memory

Flash memory has critical drawbacks such as long latency of its write operation and a short life cycle. In order to overcome these limitations, the number of write operations to flash memory devices needs to be minimized. The B-Tree index structure, which is a popular hard disk based index structure, requires an excessive number of write operations when updating it to flash memory. To address this, it was proposed that another layer that emulates a B-Tree be placed between the flash memory and B-Tree indexes. This approach succeeded in reducing the write operation count, but it greatly increased search time and main memory usage. This paper proposes a B-Tree index extension that reduces both the write count and search time with limited main memory usage. First, we designed a buffer that accumulates update requests per leaf node and then simultaneously processes the update requests of the leaf node carrying the largest number of requests. Second, a type of header information was written on each leaf node. Finally, we made the index automatically control each leaf node size. Through experiments, the proposed index structure resulted in a significantly lower write count and a greatly decreased search time with less main memory usage, than placing a layer that emulates a B-Tree.     

An index management using CHC-cluster for flash memory databases

Flash memories are one of the best media to support portable and desktop computers’ storage areas. Their features include non-volatility, low power consumption, and fast access time for read operations, features which are sufficient to present flash memories as major database storage components for portable computers. However, we need to improve traditional index management schemes based on B-Tree due to the relatively slow characteristics of flash memory operations compared to RAM memory. In order to achieve this goal, we propose a new index management scheme based on a compressed hot-cold clustering called CHC-Tree. The CHC-Tree-based index management scheme improves index operation performance by compressing the flash index nodes and clustering the hot-cold segments. The cold cluster compression techniques using unused free area in index node reduces the number of slow write operations in index node insert/delete processes. Our performance evaluation shows that our scheme significantly reduces the write operation overheads, improving the index update performance of B-Tree by 21.9%.     

FeGC: An efficient garbage collection scheme for flash memory based storage systems

NAND flash memory is a promising storage media that provides low-power consumption, high density, high performance, and shock resistance. Due to these versatile features, NAND flash memory is anticipated to be used as storage in enterprise-scale systems as well as small embedded devices. However, unlike traditional hard disks, flash memory should perform garbage collection that consists of a series of erase operations. The erase operation is time-consuming and it usually degrades the performance of storage systems seriously. Moreover, the number of erase operations allowed to each flash memory block is limited. This paper presents a new garbage collection scheme for flash memory based storage systems that focuses on reducing garbage collection overhead, and improving the endurance of flash memory. The scheme also reduces the energy consumption of storage systems significantly. Trace-driven simulations show that the proposed scheme performs better than various existing garbage collection schemes in terms of the garbage collection time, the number of erase operations, the energy consumption, and the endurance of flash memory.