Searcharxiv⌕ Search

arXiv subjects

Fuyuan Zhang

Publications and source records attributed to Fuyuan Zhang.

23 records · Page 2Linked to original sources

Combinatorial Testing for Deep Learning Systems

Deep learning (DL) has achieved remarkable progress over the past decade and been widely applied to many safety-critical applications. However, the robustness of DL systems recently receives great concerns, such as adversarial examples against computer vision systems, which could potentially result in severe consequences. Adopting testing techniques could help to evaluate the robustness of a DL system and therefore detect vulnerabilities at an early stage. The main challenge of testing such systems is that its runtime state space is too large: if we view each neuron as a runtime state for DL, then a DL system often contains massive states, rendering testing each state almost impossible. For traditional software, combinatorial testing (CT) is an effective testing technique to reduce the testing space while obtaining relatively high defect detection abilities. In this paper, we perform an exploratory study of CT on DL systems. We adapt the concept in CT and propose a set of coverage criteria for DL systems, as well as a CT coverage guided test generation technique. Our evaluation demonstrates that CT provides a promising avenue for testing DL systems. We further pose several open questions and interesting directions for combinatorial testing of DL systems.

cs.SE↗

Compositional Reasoning for Shared-variable Concurrent Programs

Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our framework models concurrent programs as succinct automata and supports the verification of multiple important properties. Safety verification and simulations of succinct automata are parallel compositional, and safety properties of succinct automata are preserved under refinements. We generate succinct automata from infinite state concurrent programs in an automated manner. Furthermore, we propose the first automated approach to checking rely-guarantee based simulations between infinite state concurrent programs. We have prototyped our algorithms and applied our tool to the verification of multiple refinements.

cs.FL↗

Refinement-based Specification and Security Analysis of Separation Kernels

Assurance of information-flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for improving safety, ARINC 653 has been complied with by mainstream separation kernels. Due to the new trend of integrating safe and secure functionalities into one separation kernel, security analysis of ARINC 653 as well as a formal specification with security proofs are thus significant for the development and certification of ARINC 653 compliant Separation Kernels (ARINC SKs). This paper presents a specification development and security analysis method for ARINC SKs based on refinement. We propose a generic security model and a stepwise refinement framework. Two levels of functional specification are developed by the refinement. A major part of separation kernel requirements in ARINC 653 are modeled, such as kernel initialization, two-level scheduling, partition and process management, and inter-partition communication. The formal specification and its security proofs are carried out in the Isabelle/HOL theorem prover. We have reviewed the source code of one industrial and two open-source ARINC SK implementations, i.e. VxWorks 653, XtratuM, and POK, in accordance with the formal specification. During the verification and code review, six security flaws, which can cause information leakage, are found in the ARINC 653 standard and the implementations.

cs.SE↗

High-Assurance Separation Kernels: A Survey on Formal Methods

Separation kernels provide temporal/spatial separation and controlled information flow to their hosted applications. They are introduced to decouple the analysis of applications in partitions from the analysis of the kernel itself. More than 20 implementations of separation kernels have been developed and widely applied in critical domains, e.g., avionics/aerospace, military/defense, and medical devices. Formal methods are mandated by the security/safety certification of separation kernels and have been carried out since this concept emerged. However, this field lacks a survey to systematically study, compare, and analyze related work. On the other hand, high-assurance separation kernels by formal methods still face big challenges. In this paper, an analytical framework is first proposed to clarify the functionalities, implementations, properties and standards, and formal methods application of separation kernels. Based on the proposed analytical framework, a taxonomy is designed according to formal methods application, functionalities, and properties of separation kernels. Research works in the literature are then categorized and overviewed by the taxonomy. In accordance with the analytical framework, a comprehensive analysis and discussion of related work are presented. Finally, four challenges and their possible technical directions for future research are identified, e.g. specification bottleneck, multicore and concurrency, and automation of full formal verification.

cs.SE↗

Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication

Assurance of information flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for separation kernels, ARINC 653 has been complied with by mainstream separation kernels. Security of functionalities defined in ARINC 653 is thus very important for the development and certification of separation kernels. This paper presents the first effort to formally specify and verify separation kernels with ARINC 653 channel-based communication. We provide a reusable formal specification and security proofs for separation kernels in Isabelle/HOL. During reasoning about information flow security, we find some security flaws in the ARINC 653 standard, which can cause information leakage, and fix them in our specification. We also validate the existence of the security flaws in two open-source ARINC 653 compliant separation kernels.

cs.SE↗