PRDC 2018: THE 23RD IEEE PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING
PROGRAM FOR WEDNESDAY, DECEMBER 5TH
Days:
previous day
next day
all days

View: session overviewtalk overview

09:30-10:30 Session 1: Keynote I
09:30
Kicking and Fixing Software: The Fun & Science of Experimental Approaches

ABSTRACT. The perpetual elusiveness of correct-by-design software fosters the need of techniques to "find and fix" software deficiencies whether they arise from design, operational or deliberate instances. Operating Systems are of particular interest given the software size, complexity and their need to operate for a wide range of stresses. With the intent of post-design software fixes, the talk ruminates on the fun, value and science of experimental techniques to "kick n' fix" software.

10:30-11:00Coffee Break
11:00-12:30 Session 2A: Hardware Reliability
11:00
Do Nothing, but Carefully: Fault Tolerance with Timing Guarantees for Multiprocessor Systems devoid of Online Adaptation

ABSTRACT. Many practical real-time systems must be able to sustain several reliability threats induced by their physical envi- ronments that cause short-term abnormal system behavior, such as transient faults. To cope with this change of system behavior, online adaptions, which may introduce a high computation overhead, are performed in many cases to ensure the timeliness of the more important tasks while no guarantees are provided for the less important tasks. In this work, we propose a system model which does not require any online adaption, but, according to the concept of dynamic real-time guarantees, provides full timing guarantees as well as limited timing guarantees, depending on the system behavior. For the normal system behavior, timeliness is guaranteed for all tasks; otherwise, timeliness is guaranteed only for the more important tasks while bounded tardiness is ensured for the less important tasks. Aiming to provide such dynamic timing guarantees, we propose a suitable system model and discuss, how this can be established by means of partitioned as well as semi-partitioned strategies. Moreover, we propose an approach for handling abnormal behavior with a longer duration, such as intermittent faults or overheating of processors, by performing task migration in order to compensate the affected system component and to increase the system’s reliability. We show by comprehensive experiments that good acceptance ratios can be achieved under partitioned scheduling, which can be further improved under semi-partitioned strategies. In addition, we demonstrate that the proposed migration techniques lead to a reasonable trade-off between the decrease in schedulability and the gain in robustness of the system. The presented approaches can also be applied to mixed-criticality systems with two criti- cality levels.

11:30
Degradable restructuring of mesh-connected processor arrays with spares on orthogonal sides

ABSTRACT. We present a restructuring method to apply a degradation approach to mesh-connected processor arrays with spare processing elements on the orthogonal sides of the arrays. An array with faulty processing elements is restructured by shifting healthy processing elements toward faulty processing elements using single track switches. First, an algorithm which satisfies a necessary and sufficient condition (called a restructurable condition) that an array is restructured so that its logical size is kept is given. Next, a method that if the array does not satisfy the restructurable condition, its rows and/or columns are functionally deleted so that the subarray with the remaining rows and columns satisfies the restructurable condition is presented.

12:00
SSCMSD - Single-Symbol Correction Multi-Symbol Detection for DRAM subsystem

ABSTRACT. As DRAM technology continues to evolve towards smaller feature sizes and increased densities, faults in DRAM subsystem are becoming more severe. Current servers mostly use CHIPKILL based schemes to tolerate up-to one/two symbol errors per DRAM beat. Multi-symbol errors arising due to faults in multiple data buses and chips may not be detected by these schemes. In this paper, we introduce Single Symbol Correction Multiple Symbol Detection (SSCMSD) - a new error handling scheme to correct single-symbol errors and detect multi-symbol errors. By using a hash in combination with ECC, we can avoid silent data corruptions in the presence of multi-symbol errors.

We employ 32-bit Spookyhash along with Reed Solomon code to implement SSCMSD for a x4 based DDRx memory system. Our simulations show that the proposed scheme effectively prevents Silent Data Corruptions in the presence of multi-symbol errors. For this design, we need a total of 19 chips per rank (storage overhead of 18.75%), 76 data bus-lines and additional hash-logic at the memory controller.

11:00-12:30 Session 2B: Information Security
11:00
Exploring the Relationship Between Dimensionality Reduction and Private Data Release

ABSTRACT. It is important to facilitate data sharing between data owners and data analysts as data owners does not always have the ability to process and analyze data. For example, governments around the world are starting to release collected data to the public to leverage data analysis competence of the crowd. However, some privacy leakage incidents have made the public to rediscover the importance of privacy protection, leading to new privacy regulations. In existing researches dimensionality reduction has played an important role in private data release mechanisms to improve utility but its influence on privacy protection has never been examined. In this study we perform a series of experiments and found that dimensionality reduction could provide similar privacy protection effects as K-anonymity mechanisms, and it could work as a preprocessor of K-anonymity process to it to reduce the generalization and suppression needed.

11:30
A certificateless one-way group key agreement protocol for end-to-end email encryption

ABSTRACT. Over the years, email has evolved into one of the most widely used communication channels for both individuals and organizations. However, despite near ubiquitous use in much of the world, current information technology standards do not place emphasis on email security. Not until recently, webmail services such as Yahoo’s mail and Google’s gmail started to encrypt emails for privacy protection. However, the encrypted emails will be decrypted and stored in the service provider’s servers. If the servers are malicious or compromised, all the stored emails can be read, copied and altered. Thus, there is a strong need for end-to-end (E2E) email encryption to protect email user’s privacy. In this paper, we present a certificateless one-way group key agreement protocol with the following features, which are suitable to implement E2E email encryption: (1) certificateless and thus there is no key escrow problem and no public key certificate infrastructure is required; (2) oneway group key agreement and thus no back-and-forth message exchange is required; and (3) n-party group key agreement (not just 2- or 3-party). This paper also provides a security proof for the proposed protocol using “proof by simulation”. Finally, efficiency analysis of the protocol is presented at the end of the paper.

12:00
InfoLeak: Scheduling-based Information Leakage

ABSTRACT. Covert- and side-channel attacks, typically enabled by the usage of shared resources, pose a serious threat to complex systems such as the Cloud. While their exploitation in the real world depends on properties of the execution environment (e.g., scheduling), the explicit consideration of these factors is often neglected. This paper introduces InfoLeak, an information leakage model that establishes the crucial role of the scheduler for exploiting core-private caches as covert channels. We show, formally and empirically, how the availability of these channels and the corresponding attack feasibility are affected by scheduling. Moreover, our model allows security experts to assess the related threat, posed by core-private cache covert channels for a particular system by considering solely the scheduling information. To validate the utility of InfoLeak, we deploy a covert-channel attack and correlate its success ratio to the scheduling of the attacker processes in the target system. We demonstrate the applicability of the InfoLeak model for analyzing the scheduling information for possible information leakage and also provide an example on its usage.

12:30-14:00Lunch Break
14:00-15:30 Session 3A: Cyber-Physical Systems
14:00
Experimental Resilience Assessment of An Open-Source Driving Agent

ABSTRACT. Autonomous vehicles (AV) depend on the sensors like RADAR and camera for the perception of environment, path planning, and control. With the increasing autonomy and interactions with the complex environment, there has been growing concerns regarding the safety and reliability of AVs. This paper presents a Systems-Theoretic Process Analysis (STPA) based fault injection framework to assess the resilience of an open-source driving agent, called openpilot, under different environmental conditions and faults affecting sensor data. To increase the coverage of unsafe scenarios during testing, we use a strategic software fault-injection approach where the triggers for injecting the faults are derived from the unsafe scenarios identified during the high-level hazard analysis of the system. The experimental results show that the proposed strategic fault injection approach increases the hazard coverage compared to random fault injection and, thus, can help with a more effective simulation of safety-critical faults and testing of AVs. In addition, the paper provides insights on the performance of openpilot safety mechanisms and its ability in timely detection and recovery from faulty inputs.

14:30
Cyber-Physical Transactions: A Method for Securing VANETs with Blockchains

ABSTRACT. Blockchains are used to perform state agreement in a distributed system. However, there is no way to validate off-chain actions, such as physical actions, in the current architecture. This paper proposes a new blockchain architecture which features locally physically verified transactions. From this new architecture, this paper presents a protocol for securing vehicular ad-hoc networks (VANETs) without the need to constantly communicate with roadside units (RSUs) or other infrastructure components. Additionally, this paper shows the results from some simple simulations of the current system in order to note its weaknesses. The paper then outlines future research areas.

15:00
Cyber-Physical Security of an Electric Microgrid

ABSTRACT. Cyber-Physical Systems (CPS) are physical systems that are controlled or monitored by computer-based systems. CPS are a combination of computation, networking, and physical processes. As CPS are a combination of various diverse components, they are vulnerable to several security threats. Moreover, there are many different security domains (not just high/low, nor are they necessarily hierarchical). This paper utilizes previouslydeveloped Multiple Security Domain Nondeducibility to uncover potential integrity vulnerabilities in an electric microgrid. These are then mitigated, to the extent possible, by adding executable invariants on system operation. Implementation on the Electric Power and Intelligent Control (EPIC) testbed at the Singapore University of Technology and Design are reported. Limitations of the design and successes/shortcomings of attack mitigation are reported.

14:00-15:30 Session 3B: Modeling
14:00
An Approach for Trustworthiness Benchmarking using Software Metrics

ABSTRACT. Trustworthiness is a paramount concern for users and customers in the selection of a software solution, specially in the context of complex and dynamic environments, such as Cloud and IoT. However, assessing and benchmarking trustworthiness (worthiness of software for being trusted) is a challenging task, mainly due to the variety of application scenarios (e.g., businesscritical, safety-critical), the large number of determinative quality attributes (e.g., security, performance), and last, but foremost, due to the subjective notion of trust and trustworthiness. In this paper, we present trustworthiness as a measurable notion in relative terms based on security attributes and propose an approach for the assessment and benchmarking of software. The main goal is to build a trustworthiness assessment model based on software metrics (e.g., Cyclomatic Complexity, CountLine, CBO) that can be used as indicators of software security. To demonstrate the proposed approach, we assessed and ranked several files and functions of the Mozilla Firefox project based on their trustworthiness score and conducted a survey among several software security experts in order to validate the obtained rank. Results show that our approach is able to provide a sound ranking of the benchmarked software.

14:30
Economic Analysis of Blockchain Technology on Digital Platform Market

ABSTRACT. Blockchain technology on the platform business becomes a new paradigm which gets security, irreversibility, and trustfulness closer to both of clients and service providers (SPs) for providing a better quality of service. To provide an economic analysis of such blockchain-based platform business, a game theoretic approach is used to model a competitive market against the incumbent platform operated by a centralizer as a trusted third party. In this market, the platforms behave as a mediator to deliver the services provided by SPs to clients. The crucial factors for the success of blockchain-based platform business are (i) how SPs' participation is reflected on its quality of service (QoS) and (ii) how to incentivize SPs to contribute their resources such as computing/storage infrastructure. In our game formulation, a non-cooperative two-stage dynamic game is used, where the first stage models how to incentivize SPs in a blockchain-based platform and the second stage models the competition between platforms to attract clients. As a result, we provide an equilibrium analysis, which gives a useful insight into how much the service quality of blockchain-based platform affects on the competition between platforms and the equilibrium incentive strategy for SPs. Moreover, our numerical analysis shows that the equilibrium incentive increases with proportional to the QoS of a blockchain-based platform whereas the incentive becomes negative if it provides a non-increasing QoS with the number of participated SPs.

14:40
Specification and Formal Verification of Atomic Concurrent Real-Time Transactions

ABSTRACT. Although atomicity, isolation and temporal correctness are crucial to the dependability of many real-time database-centric systems, the selected assurance mechanism for one property may breach another. Trading off these properties requires to specify and analyze their dependencies, together with the selected supporting mechanisms (abort recovery, concurrency control, and scheduling), which is still insufficiently supported. In this paper, we propose a UML profile, called UTRAN, for specifying atomic concurrent real-time transactions, with explicit support for all three properties and their supporting mechanisms. We also propose a pattern-based modeling framework, called UPPCART, to formalize the transactions and the mechanisms specified in UTRAN, as UPPAAL timed automata. Various mechanisms can be modeled flexibly using our reusable patterns, after which the desired properties can be verified by the UPPAAL model checker. Our techniques facilitate systematic analysis of atomicity, isolation and temporal correctness trade-offs with guarantee, thus contributing to a dependable real-time database system.

15:30-16:00Coffee Break
16:00-17:00 Session 4A: Cyber-Physical Systems
Chair:
16:00
An Approach for Formal Analysis of the Security of a Water Treatment Testbed

ABSTRACT. An increase in the number of attacks on cyberphysical systems (CPS) has raised concerns over the vulnerability of critical infrastructure such as water treatment, oil, gas plants, against cyber attacks. Such systems are controlled by an Industrial Control System (ICS) that includes controllers communicating with each other, and with physical sensors and actuators, using a communications network. This paper focuses on Multiple Security Domain Nondeducibility (MSDND) model to identify the vulnerable points of attack on the system that hide critical information rather than steal it, such as in the STUXNET virus. It is shown how MSDND analysis, conducted on a realistic multi-stage water treatment testbed, is useful in enhancing the security of a water treatment plant. Based on the MSDND analysis, this work offers a thorough documentation on the vulnerable points of attack, invariants used for removing the vulnerabilities, and suggested design decisions that help in developing invariants.

16:30
Determining the Tolerable Attack Surface that Preserves Safety of Cyber-Physical Systems

ABSTRACT. As safety-critical systems become increasingly interconnected, a system's operations depend on the reliability and security of the computing components and the interconnections among them. Therefore, a growing body of research seeks to tie safety analysis to security analysis. Specifically, it is important to analyze system safety under different attacker models. In this paper, we develop generic parameterizable state automaton templates to model the effects of an attack. Then, given an attacker model, we generate a state automaton that represents the system operation under the threat of the attacker model. We use a railway signaling system as our case study and consider threats to the communication protocol and the commands issued to physical devices. Our results show that while less skilled attackers are not able to violate system safety, more dedicated and skilled attackers can affect system safety. We also consider several countermeasures and show how well they can deter attacks.

16:00-17:00 Session 4B: Modeling
16:00
Modeling the Required Indoor Temperature Change by Hybrid Automata for Detecting Thermal Problems

ABSTRACT. Hybrid automata are a formal model for dynamical systems with discrete and continuous components. This paper exploits the capability of hybrid automata to model the required indoor temperature change for comprehensively detecting thermal problems. The requirement is to specify the changes in the indoor temperature by considering thermal discomfort that ranges from uncomfortable to serious. We first devise an example of home appliance control service for indoor temperature adjustment. Then, based on the example, this paper proposes the modeling of the required indoor temperature change by hybrid automata. To this end, we represent different states of the hybrid automata, which correspond to different thermal sensations of indoor temperature change, by resorting to various indices. Then, the required indoor temperature change is prescribed by heat exchange between indoor and outdoor. Experiment results demonstrate the capability of hybrid automata to model the required indoor temperature change.

16:30
Software Test-Run Reliability Modeling with Non-homogeneous Binomial Processes

ABSTRACT. While the number of test runs (test cases) is often used to define the time scale to measure quantitative software reliability, the common calendar-time modeling with non-homogeneous Poisson processes (NHPPs) is approximately applied to describe the time scale and the software fault-count phenomena as well. In this paper we give a conjecture that such an approximate treatment is not theoretically justified, and propose a simple test-run reliability modeling framework based on non-homogeneous binomial processes (NHBPs). We show that the Poisson-binomial distribution plays a central role in the software test-run reliability modeling, and apply it to the software release decision. In numerical experiments with seven software fault count data we compare the NHBP based software reliability models (SRMs) with their corresponding NHPP based SRMs and refer to an applicability of NHBP based software test-run reliability modeling.