Solid-state drives (SSDs) are fast emerging as the primary choice for data storage in diverse domains. However, data protection against ransomware attacks on such storage devices is a crucial challenge. A recent research work proposed an In-SSD ransomware protection mechanism to improve SSD data security. The SSD flash translation layer (FTL), which consists of an address mapping, garbage collection, and wear leveling components, is inherently the most complex part of an SSD controller. The In-SSD ransomware protection mechanism adds a new component to the FTL, making the FTL design more complex. The new component interacts with almost all other units of FTL for recovery from a ransomware attack. Such a design would naturally require rigorous verification, which is the focus of this article. In this work, we discuss the derivation of a set of security properties related to protection from ransomware that covers the security requirements and the design; we next prove such properties using symbolic model checking.

Modern NVMe SSDs are widely deployed in diverse domains due to characteristics like high performance, robustness, and energy efficiency. It has been observed that the impact of interference among the concurrently running workloads on their overall response time differs significantly in these devices, which leads to unfairness. Workload intensity is a dominant factor influencing the interference. Prior works use a threshold value to characterize a workload as high-intensity or low-intensity; this type of characterization has drawbacks due to lack of information about the degree of low- or high-intensity.

The leakage power dissipation has become one of the major concerns with technology scaling. The GPGPU register file has grown in size over last decade in order to support the parallel execution of thousands of threads. Given that each thread has its own dedicated set of physical registers, these registers remain idle when corresponding threads go for long latency operation. Existing research shows that the leakage energy consumption of the register file can be reduced by under volting the idle registers to a data-retentive low-leakage voltage (Drowsy Voltage) to ensure that the data is not lost while not in use. In this paper, we develop a realistic model for determining the wake-up time of registers from various under-volting and power gating modes. Next, we propose a hybrid energy saving technique where a combination of power-gating and under-volting can be used to save optimum energy depending on the idle period of the registers with a negligible performance penalty. Our simulation shows that the hybrid energy-saving technique results in 94% leakage energy savings in register files on an average when compared with the conventional clock gating technique and 9% higher leakage energy saving compared to the state-of-art technique.

Formal modeling and analysis of a victim DRAM cache has already been discussed in the existing literature. These works use interacting state machines to model states and transitions of a victim DRAM cache. In this work, we address model-code conformance between a formal model of the victim DRAM cache and a simulator obtained from it. Our work focuses on a two-step approach to validate a DRAM cache implementation. In the first step, we use a technique based on it Feedback-Directed Random Testing to reverse engineer the state models from the execution traces. This process helps us to match the implementation with the state machines associated with the formal model and to verify some of the state-based properties. In the second step, we instrument the implementation with monitors and validate the liveness and safety properties (during run-time) which have been proved earlier in the formal model.

NAND flash memory has become the de facto standard for several non-volatile storages used in commercial and mission-critical applications. The advanced operations supported by NAND flash memory contribute to device performance and also influence the design of some of the crucial mechanisms of the flash memory device controller. In this research, we consider a recent ONFI standard i.e. ONFI-3.2 and successfully model the NAND flash memory device with the advanced operations in addition to many basic operations in contrast to the existing research works. We encode all the properties obtained from the standard in LTL and proved those using symbolic model checking. Our modeling approach simplifies the state machines and reduces resource requirements while capturing the essential information needed to verify the requirement based properties.

The emerging Die-stacking technology enables DRAM to be used as a cache to break the “Memory Wall” problem. Recent studies have proposed to use DRAM as a victim cache in both CPU and GPU memory hierarchies to improve performance. DRAM caches are large in size and, hence, when realized as a victim cache, non-inclusive design is preferred. This non-inclusive design adds significant differences to the conventional DRAM cache design in terms of its probe, fill, and writeback policies. Design and verification of a victim DRAM cache can be much more complex than that of a conventional DRAM cache. Hence, without rigorous modeling and formal verification, ensuring the correctness of such a system can be difficult. The major focus of this work is to show how formal modeling is applied to design and verify a victim DRAM cache. In this approach, we identify the agents in the victim DRAM cache design and model them in terms of interacting state machines. We derive a set of properties from the specifications of a victim cache and encode them using Linear Temporal Logic. The properties are then proven using symbolic and bounded model checking. Finally, we discuss how these properties are related to the dataflow paths in a victim DRAM cache.

GPGPUs are now commonly used as co-processors of CPUs for the computation of data parallel and throughputintensive algorithms. However, memory available in GPGPUs is limited for many applications of interest; there is a continuous demand for increased memory of such applications. Several techniques like multi-steaming or pinned memory are frequently employed to mitigate these issues to some extent. However, these techniques either suffer from latency overhead or increase programming complexity. GPUdmm uses GPU DRAM as a cache of CPU; key problems in this design are inefficient memory access data-path and tag access overhead. In this context, we present CAMO, a novel cache memory organization for GPGPUs which addresses the limitations of pinned memory technique and GPUdmm. First, it uses GPU DRAM as a victim cache of LLC that improves the performance by delivering data faster to the SMs. Second, it uses ATCache, a CPU based DRAM cache tag management technique. ATCache reduces the number of DRAM cache accesses. We implement CAMO within the GPGPU-Sim framework and show that its average performance - when compared with pinned memory - increases by a factor of 1.87x and the peak performance growth being 4.67x. In addition, CAMO outperforms GPUdmm on an average by a factor of 15.9% and maximum speedup by a factor of 80%.

Die-stacking technology enables the use of a high density DRAM as a cache. Major processor vendors have recently started using these stacked DRAM modules as the last level cache of their products. These stacked DRAM modules provide high bandwidth with relatively low latency compared to the off-package DRAM modules. Recent studies on DRAM caches propose several variants to optimize performance and power of the systems. However, none of the existing works discuss its design and verification aspect. DRAM cache controller (DCC) design is significantly complex in comparison to a conventional DRAM-based main memory controller. This is because it involves controlling both the timing aspect of DRAM system as well as the functional aspect of cache. Therefore, without rigorous modeling and verification of such designs, it would be difficult to ensure correctness. In the current research, we focus on the design and verification issues of DCC. We select a common variant of DRAM cache and build a formal model of its controller in terms of interacting state machines; we term the common variant as the baseline and its model as the base model. We then verify safety, liveness, and timing properties of this variant using model checking. Next, we demonstrate how the formal models and the associated properties of other variants of DCCs can be derived from the base model in a systematic way. Analyzing the individual DRAM cache variations, we observe that most of the variants exhibit product-line characteristics.