Cloud Building Block Chip for Creating FPGA and ASIC Clouds

Hardware-accelerated cloud computing systems based on FPGA chips (FPGA cloud) or ASIC chips (ASIC cloud) have emerged as a new technology trend for power-efficient acceleration of various software applications. However, the operating systems and hypervisors currently used in cloud computing will lead to power, performance, and scalability problems in an exascale cloud computing environment. Consequently, the present study proposes a parallel hardware hypervisor system that is implemented entirely in special-purpose hardware, and that virtualizes application-specific multi-chip supercomputers, to enable virtual supercomputers to share available FPGA and ASIC resources in a cloud system. In addition to the virtualization of multi-chip supercomputers, the system’s other unique features include simultaneous migration of multiple communicating hardware tasks, and on-demand increase or decrease of hardware resources allocated to a virtual supercomputer. Partitioning the flat hardware design of the proposed hypervisor system into multiple partitions and applying the chip unioning technique to its partitions, the present study introduces a cloud building block chip that can be used to create FPGA or ASIC clouds as well. Single-chip and multi-chip verification studies have been done to verify the functional correctness of the hypervisor system, which consumes only a fraction of (10%) hardware resources.

Model Checking M2M and Centralised IOT authentication Protocols.

It is very difficult to develop a perfect security protocol for communication over the IoT network and developing a reliable authentication protocol requires a detailed understanding of cryptography. To ensure the reliability of security protocols of IoT, the validation method is not a good choice because of its several disadvantages and limitations. To prove the high reliability of Cryptographic Security Protocols(CSP) for IoT networks, the functional correctness of security protocols must be proved secure mathematically. Using the Formal Verification technique we can prove the functional correctness of IoT security protocols by providing the proofs mathematically. In this work, The CoAP Machine to Machine authentication protocol and centralied IoT network Authentication Protocol RADIUS is formally verified using the well-known verification technique known as model checking technique and we have used the Scyther model checker for the verification of security properties of the respective protocols. The abstract protocol models of the IoT authentication protocols were specified in the security protocol description language and the security requirements of the authentication protocols were specified as claim events.

WaFFLe

Managing thermal imbalance in contemporary chip multi-processors (CMPs) is crucial in assuring functional correctness of modern mobile as well as server systems. Localized regions with high activity, e.g., register files, ALUs, FPUs, and so on, experience higher temperatures than the average across the chip and are commonly referred to as hotspots. Hotspots affect functional correctness of the underlying circuitry and a noticeable increase in leakage power, which in turn generates heat in a self-reinforced cycle. Techniques that reduce the severity of or completely eliminate hotspots can maintain functional correctness along with improving performance of CMPs. Conventional dynamic thermal management targets the cores to reduce hotspots but often ignores caches, which are known for their high leakage power consumption. This article presents WaFFLe , an approach that targets the leakage power of the last-level cache (LLC) and hotspots occurring at the cores. WaFFLe turns off LLC-ways to reduce leakage power and to generate on-chip thermal buffers. In addition, fine-grained DVFS is applied during long LLC miss induced stalls to reduce core temperature. Our results show that WaFFLe reduces peak and average temperature of a 16-core based homogeneous tiled CMP with up to 8.4 ֯ C and 6.2 ֯ C, respectively, with an average performance degradation of only 2.5 %. We also show that WaFFLe outperforms a state-of-the-art cache-based technique and a greedy DVFS policy.

A Method to Deduce and Synthesize the Dafny Programs

We propose a systematic method to deduce and synthesize the Dafny programs. First, the specification of problem is described in strict mathematical language. Then, the derivation process uses program specification transformation technology to perform equivalent transformation. Furthermore, Dafny program is synthesized through the obtained recursive relationship and loop invariants. Finally, the functional correctness of Dafny program is automatically verified by Dafny verifier or online tool. Through this method, we deduce and synthesize Dafny programs for many typical problems such as the cube sum problem, the minimum (or maximum) contiguous subarray problems, several searching problems, several sorting problems, and so on. Due to space limitation, we only illustrate the development process of Dafny programs for two typical problems: the minimum contiguous subarray problem and the new local bubble sorting problem. It proves that our method can effectively improve the correctness and reliability of Dafny program developed. What’s more, we demonstrate the potential of the deductive synthesis method by developing a new local bubble Sorting program.

SecRSL: security separation logic for C11 release-acquire concurrency

We present Security Relaxed Separation Logic (SecRSL), a separation logic for proving information-flow security of C11 programs in the Release-Acquire fragment with relaxed accesses. SecRSL is the first security logic that (1) supports weak-memory reasoning about programs in a high-level language; (2) inherits separation logic’s virtues of compositional, local reasoning about (3) expressive security policies like value-dependent classification. SecRSL is also, to our knowledge, the first security logic developed over an axiomatic memory model. Thus we also present the first definitions of information-flow security for an axiomatic weak memory model, against which we prove SecRSL sound. SecRSL ensures that programs satisfy a constant-time security guarantee, while being free of undefined behaviour. We apply SecRSL to implement and verify the functional correctness and constant-time security of a range of concurrency primitives, including a spinlock module, a mixed-sensitivity mutex, and multiple synchronous channel implementations. Empirical performance evaluations of the latter demonstrate SecRSL’s power to support the development of secure and performant concurrent C programs.

Fully automated functional fuzzing of Android apps for detecting non-crashing logic bugs

Android apps are GUI-based event-driven software and have become ubiquitous in recent years. Obviously, functional correctness is critical for an app’s success. However, in addition to crash bugs, non-crashing functional bugs (in short as “non-crashing bugs” in this work) like inadvertent function failures, silent user data lost and incorrect display information are prevalent, even in popular, well-tested apps. These non-crashing functional bugs are usually caused by program logic errors and manifest themselves on the graphic user interfaces (GUIs). In practice, such bugs pose significant challenges in effectively detecting them because (1) current practices heavily rely on expensive, small-scale manual validation ( the lack of automation ); and (2) modern fully automated testing has been limited to crash bugs ( the lack of test oracles ). This paper fills this gap by introducing independent view fuzzing , a novel, fully automated approach for detecting non-crashing functional bugs in Android apps. Inspired by metamorphic testing, our key insight is to leverage the commonly-held independent view property of Android apps to manufacture property-preserving mutant tests from a set of seed tests that validate certain app properties. The mutated tests help exercise the tested apps under additional, adverse conditions. Any property violations indicate likely functional bugs for further manual confirmation. We have realized our approach as an automated, end-to-end functional fuzzing tool, Genie. Given an app, (1) Genie automatically detects non-crashing bugs without requiring human-provided tests and oracles (thus fully automated ); and (2) the detected non-crashing bugs are diverse (thus general and not limited to specific functional properties ), which set Genie apart from prior work. We have evaluated Genie on 12 real-world Android apps and successfully uncovered 34 previously unknown non-crashing bugs in their latest releases — all have been confirmed, and 22 have already been fixed. Most of the detected bugs are nontrivial and have escaped developer (and user) testing for at least one year and affected many app releases, thus clearly demonstrating Genie’s effectiveness. According to our analysis, Genie achieves a reasonable true positive rate of 40.9%, while these 34 non-crashing bugs could not be detected by prior fully automated GUI testing tools (as our evaluation confirms). Thus, our work complements and enhances existing manual testing and fully automated testing for crash bugs.

Demonstration of Shor’s factoring algorithm for N $$=$$ 21 on IBM quantum processors

We report a proof-of-concept demonstration of a quantum order-finding algorithm for factoring the integer 21. Our demonstration involves the use of a compiled version of the quantum phase estimation routine, and builds upon a previous demonstration. We go beyond this work by using a configuration of approximate Toffoli gates with residual phase shifts, which preserves the functional correctness and allows us to achieve a complete factoring of $$N=21$$ N = 21 . We implemented the algorithm on IBM quantum processors using only five qubits and successfully verified the presence of entanglement between the control and work register qubits, which is a necessary condition for the algorithm’s speedup in general. The techniques we employ may be useful in carrying out Shor’s algorithm for larger integers, or other algorithms in systems with a limited number of noisy qubits.

A Framework for Model and Verification of Safety-Critical Operating System Based on ARINC653

As the scale and complexity of safety-critical software continue to grow, it is necessary to ensure safety and reliability to avoid minor errors leading to catastrophic disasters. Meantime, the traditional method, such as testing and simulation alone is insufficient to ensure the correctness of systems. This leads to using formal methods to provide sufficient evidence for systems. However, design a high assurance safety-critical system by formal methods is challenging due to the complexity of operating systems. In addition, the traditional interactive theorem prover used in system verification requires hand-written proofs, which are more expensive. Therefore, the efforts of providing a standardized formal framework as well as safety proofs, are notable for the develop a safety-critical system. The purpose of this paper is to provide a safety framework to establish a highly reliable and safety-critical operating system based on the ARINC653 standard, a multilevel and standardized formal model. To verify the functional correctness of this model, we propose a context-based formal proof method for programs. To achieve this goal, we first model 57 core services of ARINC653 and define the high-level requirements as pre-and post-conditions. Then, we construct a set of specification statements a formal axiom system transformed into logical sentences, and the core service model is transformed into a logical sentence sequence to be proved. Finally, a context-based formal proof system for specification correctness is developed. We have verified the correctness of safety-critical operating system core services with this system. Experience shows that the verification system we developed can be achieved the functional correctness of a complete OS with a low implement burden, and that can simplify the difficulty of automated verification and increase the degree of automation of proof.

Analysis of Functional Suitability and Usability in Sales Order Procedure to Determine Management Information System Quality

In the development of information systems, it is very important to pay attention to the quality of the system which can be reviewed through aspects of usability for its users and following the needs and specifications of its users. This study will analyze the quality of the sales order management information system based on two characteristics of the ISO 25010 quality standard system, namely functional suitability and usability. The functional suitability test was carried out by the BlackBox testing method to test three sub-characteristics of functional suitability that are functional completeness, functional correctness, and functional appropriateness. Usability tests use a use questionnaire which is divided into four criteria that are usefulness, ease of use, ease of learning, and satisfaction. In testing the suitability of functionality involving 5 respondents and 17 respondents in usability testing. The results of this study indicate that the sales order management system fulfills two characteristics of information system quality that are functional suitability and usability. Where all the features designed are by the successful features, and the usability characteristics are 85.45% which indicates that the system is very feasible to implement.

Multi-armed Bandit Algorithms on System-on-Chip: Go Frequentist or Bayesian?

Multi-armed Bandit (MAB) algorithms identify the best arm among multiple arms via exploration-exploitation trade-off without prior knowledge of arm statistics. Their usefulness in wireless radio, IoT, and robotics demand deployment on edge devices, and hence, a mapping on system-on-chip (SoC) is desired. Theoretically, the Bayesian approach-based Thompson Sampling (TS) algorithm offers better performance than the frequentist approach-based Upper Confidence Bound (UCB) algorithm. However, TS is not synthesizable due to \textit{Beta} function. We address this problem by approximating it via a pseudo-random number generator-based approach and efficiently realize the TS algorithm on Zynq SoC. In practice, the type of arms distribution (e.g., Bernoulli, Gaussian, etc.) is unknown and hence, a single algorithm may not be optimal. We propose a reconfigurable and intelligent MAB (RI-MAB) framework. Here, intelligence enables the identification of appropriate MAB algorithms for a given environment, and reconfigurability allows on-the-fly switching between algorithms on the SoC. This eliminates the need for parallel implementation of algorithms resulting in huge savings in resources and power consumption. We analyze the functional correctness, area, power, and execution time of the proposed and existing architectures for various arm distributions, word-length, and hardware-software co-design approaches. We demonstrate the superiority of the RI-MAB over TS and UCB only architectures.