High-Availability requires hardware and software redundancy. Virtualization is a technique - among others - for improving the utilization of hardware resources by making virtual (rather than actual) versions of hardware, operating system, etc. and collocating them on the same hardware. In virtualized environments virtual machines (VMs) are used for the deployment of the software entities. When VMs hosting redundant software entities providing and protecting some service are collocated on the same physical node, the hardware redundancy is lost and the failure of this physical node certainly leads to service outage. To achieve high availability, we need to avoid such single points of failure even in the presence of VM migration. This paper tackles this issue in the context of a standardized middleware for service high-availability.
Mobile devices such as smart phones and tablet PCs are becoming common personal devices. The business model of a central software market is also thriving and turning into a major distribution source of software packages on those devices. However, these devices often contain personal private information and can be used to conduct operations involving data leakage and payment events like sending SMS. As a result, the quality of software on mobile devices becomes a critical issue. We aim at checking whether software off the shelf contains defective behavior or potential vulnerabilities, and aiding the official APP or third party markets to ensure their software without privacy issues. We have built a platform for android APP testing, by revising our software quality assurance and exploit generation platform, called CRAX, to apply in the Android platform. It is called the CRAXDroid that allows any inputs to be the testing sources to the APP without source code. These approaches are based on the symbolic execution technique and android emulator. By automatically exploring execution paths, we can find potential software defects. We perform several experiments on Android applications to prove the feasibility of our method.
Since EPCglobal announced Class 1 Generation 2 tag (Gen2) as the standard tag for supply chain management applications and Gen2 was ratified as an ISO 18000-6C standard, much effort has been devoted to promoting various Gen2-based applications and improving the security of Gen2. However, as many Gen2-based applications go beyond the original supply chain management and the security requirements of these applications could not be fulfilled without modifying the original Gen2 standards, EPC Global recently (2013/11) announced the revised Gen2 standard-called Gen2 version 2 (Gen2v2 for short), Gen2v2 includes several new security and file management features to fit various possible application requirements. Inspired by these new features, Engels et al. proposed two Gen2v2-based mutual authentication schemes. In this paper, we cryptanalyze the protocols, show the security weaknesses, and proposed our improvements.
Numerical analysis is an important process for creating reliable numerical software. However, traditional analysis methods rely on manual estimation by numerical analysts, which is restricted by the problem size. Although some state-of-art software packages can check whether a program is numerical unstable, they cannot tell whether it is caused by ill-posed problem itself or by some improper implementation practices, while these packages work on the floating point values in the program. In this paper, we introduce an automatic framework that utilizes infinite-precision arithmetic to analyze large-scale numerical problems by computer. To eliminate rounding errors, the computing process iterates itself to increase intermediate precision until the calculation reaches the desired final precision. Then the framework perturbs the inputs and intermediate values of a certain numerical problem. By checking the gaps among different program outputs, the framework helps us understand whether the problem is well-conditioned or ill-conditioned. The framework also compares the infinite-precision arithmetic with fixed-precision arithmetic. The evaluation of a bunch of classical problems shows that our framework is able to detect the ill-conditioning in large-scale problems effectively.
Mobile devices are becoming increasingly general-purpose, and therefore the physical boundary used to separate important resources disappears. As a result, malicious applications (apps) get chances to abuse resources that are available on the mobile platform. In this paper, we propose resource virtualization as a security mechanism for the Android system to strengthen the physical barrier between many types of resources and confine resource-abusing Android apps. The physical resources on a mobile device are virtualized to a different virtual view for selected Android apps. Resource virtualization simulates a partial but consistent virtual view of the Android resources. Therefore, it can not only confine the resource-abusing apps effectively, but also ensure the usability of these apps. We implement a system prototype, RVL, and evaluate it with real-world apps of various types. Our results demonstrate its effectiveness on malicious Android apps and its compatibility and usability on benign Android apps.
Under the increasing complexity and time-to-market pressures, functional validation is becoming a major bottleneck of smartphone applications running on mobile platforms (e.g., Android, iOS). Due to the GUI (Graphical User Interface) intensive nature, the execution of smartphone applications heavily relies on the interactions with users. Manual GUI testing is extremely slow and unacceptably expensive in practice. However, the lack of formal models of user behaviors in the design phase hinders the automation of GUI testing (i.e., test case generation and test evaluation). While thorough test efforts are required to ensure the consistency between user behavior specifications and GUI implementations, few of existing testing approaches can automatically utilize the design phase information to test complex smartphone applications. Based on UML activity diagrams, this paper proposes an automated GUI testing framework called AD Automation, which supports user behavior modeling, GUI test case generation, and post-test analysis and debugging. The experiments using two industrial smartphone applications demonstrate that our approach can not only drastically reduce overall testing time, but also improve the quality of designs.
As wireless networks being prevalent, rogue access points (AP) become a serious security issue. Among various rogue APs, a fake AP with fully forging the SSID and MAC address of a legitimate AP is the hardest thing to detect and the highest probability of causing security breach. Among the past academic papers, which scholars had published, mainly relied on statistics of packets to detect fake APs. They are apt to trigger false alarms. To measure more precisely, this research proposes an algorithm that is based on the interval, serial number, and timestamp of beacons. In our analysis, even the hackers deliberately synchronize the sequence numbers and timestamp of both legal and fake APs, we are still able to exactly identify whether a fake AP exists or not.
Software safety standards are commonly used to guide the development of safety-critical software systems. However, given the existence of multiple competing standards, it is critical to select the most appropriate one for a given project. We have developed a set of 15 criteria to evaluate each standard in terms of its usage, strengths, and limitations. Five standards are studied, including a NASA Software Safety Standard, an FAA System Safety Handbook, MIL-STD-882D (US Department of Defense), DEF-STAN 00-56 (UK Ministry of Defense), and DO-178B (Commercial avionics). Results of our evaluation suggest that different standards score differently with respect to each evaluation criterion. No standard performs better than others on all the criteria. The lessons learned from software-related accidents in which the standards were involved provide further insights on the pros and cons of using each standard.
To evade VM-based malware analysis systems, VM-aware malware equipped with the ability to detect the presence of virtual machine has appeared. To cope with the problem, detecting VM-aware malware and locating VM-sensitive divergence points of VM-aware malware is in urgent need. In this paper, we propose a novel block-based divergence locator. In contrast to the conventional instruction-based schemes, the block-based divergence locator divides malware program into basic blocks, instead of binary instructions, and uses them as the analysis unit. The block-based divergence locator significantly decrease the cost of behavior logging and trace comparison, as well as the size of behavior traces. As the evaluation showed, behavior logging is 23.87-39.49 times faster than the conventional schemes. The total number of analysis unit, which is highly related to the cost of trace comparisons, is 11.95%-16.00% of the conventional schemes. Consequently, VM-sensitive divergence points can be discovered more efficiently. The correctness of our divergence point discovery algorithm is also proved formally in this paper.
Process Algebra for Demand and Supply (shortly, PADS), proposed by Philippou et al., is a process algebra model for the formal analysis of hierarchical scheduling. They introduce a basic notion of supply simulation relation to characterize task's schedulability. In this paper, we first investigate some properties of supply simulation relation. And then based on these properties, we present a proof system for the supply simulation relation in a decomposing-composing way and prove its soundness and completeness with respect to the semantic definition of a supply simulation relation. The soundness and completeness guarantee that the proof system is used to determine whether a task is schedulable by a supply or not.
In this paper, a cache coherence scheme in multi-processor is introduced. There is a specific model in each kind of software, cache coherence can be solved in AHB bus by these models. First, we use dynamic address mapping policy to realize data cache. Second, according to the randomness of application environment that set up shared cache adaptive configuration and management mechanism in the finite state machine timing sequence model of each kind of software, to ensure the system reliability. In order to support multi-tasking and multi-user operator system - Linux, the multi-processor must use shared memory technology, so this paper also introduced the memory management unit, and base on these, it focuses on how multi-processor and the AHB bus cooperate to ensure cache coherence of the whole system. We can use software execution model and hardware design to achieve instruction or data coherence between each cache and main memory.
A multiphysics model of Micro-CVD chip for growing carbon nanotubes is presented in this paper. The proposed model covers structural, thermal and electric analyses and takes consideration of all modes of heat dissipation include heat convection, conduction and radiation. The temperature dependence of thermo physical properties and heat transfer properties are also taken into account. The method is proved to be general and can be used for the simulation and analysis of different type of electro-thermal Micro-CVD chip at different physical size over a wide range of operating temperature. Thus the thermal design of Micro-CVD chip for uniform temperature control, which is critical in synthesize carbon nanotubes, becomes possible. An improved distribution of micro-tubes on hot stage of Micro-CVD chip is designed and simulated. The temperature reaches 1300K and the variation on the whole reactive region of the hot stage is within ± 7K.
An increasing number of web applications are now hosted in cloud infrastructures such as Amazon Web Services. Cloud infrastructures generally lack a uniform guarantee on security, reliability, performance, and cost. A privately owned cloud infrastructure may be considered more secure but less performant than a third-party public cloud infrastructure. Infrastructures that span across geographical regions may further incur complications on the trustworthiness of infrastructures due to the varying power of jurisdiction. Application developers have to be aware of the non-uniformity of infrastructure trustworthiness when deploying applications in the cloud. We propose the MicroApp architecture that help address the difficulty in dealing with the non-uniformity. MicroApp splits a web application into multiple micro applications. Each micro application encapsulates a port of the code and data with the same level of security and integrity requirement. The micro applications will then be deployed to corresponding infrastructures that satisfy the respective requirements. MicroApp provides an RPC mechanism to allow control flows across micro applications. The architecture can be transparently applied to existing web applications and allows an application to effectively adapt to the cloud environment.
Firefox OS, a new Web-based OS developed by Mozilla mainly for mobile platforms, is designed to realize the " Boot to the Web" concept for the open Web. It supports users booting to the network directly, launching remote applications and accessing remote data with the standard Web technologies. Although Firefox OS has adopted several mechanisms to enhance its security, its current design is lack of a mechanism to detect 1) applications calling Web API with unusual frequency, and 2) applications consuming abnormal amount of resources. In this paper, we propose an anomaly detection module which takes the system resource usage and the amount of interprocess communication as the inputs to detect whether the system has an anomaly. We also conduct several experiments to examine the ability of the proposed module. The results show that detection accuracy of our module is 0% in false negative rate and 12.5% in false positive rate.
Runtime verification with a predictive semantics defines how to monitor a temporal property in a predictive manner. In this paper, we propose a predictive runtime verification framework for Cyber-Physical Systems (CPS), which are usually open embedded systems, aiming to predict the runtime failures of CPS before the failure really happen. We present the method for online predications based on the program information and the runtime information. We have implemented a prototype framework based on JavaMOP. The experimental results demonstrate that our framework is generally applicable.
FMECA (Failure Modes, Effects and Criticality Analysis) is an effective systematic process to evaluate software safety. In this paper, the safety model of embedded systems is built by integrating the AADL (Architecture Analysis and Design Language) model with extension of Error Model Annex, and the FMECA is adopted as a qualitative safety analysis for AADL (Architecture Analysis and Design Language) model of embedded system based on AADL safety model. The traditional FMECA method is improved to be suitable for AADL model evaluation, and some safety properties are added into AADL error model annex in order to fill in FMECA check list automatically at AADL modeling design phase. On using the OVP (Over Voltage Protection) system, a case study is demonstrated the feasibility of modified FMECA for AADL model.
The reliability and security of software are affected by its constant changes. For that reason, developers use change-impact analysis early to identify the potential consequences of changing a program location. Dynamic impact analysis, in particular, identifies potential impacts on concrete, typical executions. However, the accuracy (precision and recall) of dynamic impact analyses for predicting the actual impacts of changes has not been studied. In this paper, we present a novel approach based on sensitivity analysis and execution differencing to estimate, for the first time, the accuracy of dynamic impact analyses. Unlike approaches that only use software repositories, which might not be available or might contain insufficient changes, our approach makes changes to every part of the software to identify actually impacted code and compare it with the predictions of dynamic impact analysis. Using this approach in addition to changes made by other researchers on multiple Java subjects, we estimated the accuracy of the best method-level dynamic impact analysis in the literature. Our results suggest that dynamic impact analysis can be surprisingly inaccurate with an average precision of 47-52% and recall of 56-87%. This study offers insights to developers into the effectiveness of existing dynamic impact analyses and motivates the future development of more accurate analyses.
The basic condition of software reliability assessment is failure time, which must be acquired during a test based on operational profile or on real usage. Failure data from software development or other non-software reliability testing (SRT) cannot be used for reliability evaluation because such data do not include usage information and failure time. This paper presents a software reliability virtual test (SRVT), which constructs the software input space model and the known failure input space model through which possible failure time can be determined by matching the randomly generate inputs. An experiment comparing SRT and SRVT with different thresholds is introduced to verify SRVT. Results indicate that SRVT saves a large amount of testing time while providing reliability assessment with acceptable accuracy.
In the paper, we have proposed a local-world synchronization-preferential growth topology model. The synchronizability of a class of continuous-time local-world dynamical networks is investigated. Then it has been found that the synchronizability of the dynamical network with the local-world synchronization-preferential mechanism is robust against not only the random removal of vertices but also the specific removal of those most connected vertices.
Transforming informal specifications to formal specifications is an effective approach to clarifying user's requirements. However, how to keep the consistency between the informal specification and the formal specification is a major challenge. In this paper, we propose an inspection method for verifying whether all requirements described in an informal specification are formalized in the corresponding formal specification. Inspection is a static analysis technique based upon a checklist containing questions that should be answered. Our proposed inspection method advocates the principle that the checklist is created based on the trace ability of specifications and animation is used as a reading technique for checking through the formal specification. The trace ability reflects connections between informal and formal specifications, which can facilitate the inspector to check whether all requirements have been realized. The animation provides an intuitive way to guide the inspector in reading the formal specification. We use a case study to demonstrate how an inspection is performed.
