Abstract Formal verification of Semantic Segmentation Networks is challenging due to high-dimensional output spaces and cumulative over-approximation errors in deep architectures. Existing verification methods based on specific Star-set reachability suffer from either exponential state explosion (exact splitting) or excessive conservativeness (interval-based relaxation). In this work, we present ATKVerifier , a verification framework for SSNs operating on an abstract domain named constrained-star (C-star), which captures spatial dependencies within MaxPool receptive fields through explicit predicate constraints. Our framework features: (1) an adaptive top-K lower bound mechanism that dynamically encodes K potential maximizers based on layer depth and interval overlap, balancing precision and computational cost through parameter-free adaptation; (2) an adaptive affine upper bound exploiting linear relationships between top candidates to replace conservative constant bounds; and (3) region-level completeness (RLC), a spatial robustness metric quantifying the integrity of verified contiguous object regions. Experiments on M2NIST with three SSN architectures (16 $$\sim $$ ∼ 24 layers) demonstrate 8 $$\sim $$ ∼ 25% improvement in robust Intersection-over-Union (IoU) over the ImageStar-based NNV baseline, with the improvement scaling with the network’s depth. For the 24-layer architecture, ATKVerifier achieves 59.2% RLC versus 43.8% of NNV, certifying 35.2% more complete semantic objects.

Deep neural networks (DNNs) have become integral to numerous safety-critical applications, necessitating rigorous verification of their trustworthiness. However, the problem of verifying DNNs has high computational complexity, and existing techniques have limited efficiency, insufficient to deal with large-scale network models. To address this challenge, we propose a novel abstraction-refinement verification method that reduces network size while maintaining verification accuracy. Specifically, the method quantifies the similarity between neurons based on various factors such as their interval outputs, and then merges similar neurons to generate a smaller abstract network. In addition, a counterexample-guided refinement process is developed to mitigate the impact of potential spurious counterexamples, so that verification results from the abstract network are applicable to the original network. We have implemented this method as a tool named ARVerifier and integrated it with three state-of-the-art verification tools for evaluation on ACAS Xu and MNIST benchmarks. Experimental results demonstrate that ARVerifier significantly reduces network size and yields verification time reductions by 11.61%, 18.70%, and 12.20% compared to α,β-CROWN, Verinet, and Marabou, respectively. Moreover, ARVerifier exhibits efficiency improvements by 26.64% and 46.87% compared to existing abstraction-refinement methods NARv and CEGAR-NN, respectively.

Abstract At present, formal methods significantly facilitate the specification and verification of security requirements in requirement engineering, which can reduce requirement errors in the early stage of system development. Extracting formal specifications from security requirements and then evaluating the quality of the requirements are regarded as a promising solution to ensure software quality. Propositional projection temporal logic (PPTL) with a strong mathematical basis and full regular expressiveness is a suitable language for formal specifications. Inspired by natural language processing and text mining techniques, this paper designs and implements a tool, namely, NL2PPTL, to generate formal coarse‐grained and fine‐grained specifications in terms of PPTL formulas automatically. In specific, the grammatical production rules are defined to construct the syntax tree, and then, the formula is obtained by post‐order traversal of the tree. The satisfiability of the PPTL specifications can be checked utilizing PPTLSAT. In addition, the state transformation model is constructed from fine‐grained specifications, so as to discover scope conflicts and verify the security properties of the requirement case.

Interrupt-driven programs have been widely used in safety-critical areas such as aerospace and embedded systems. However, uncertain interleaving execution of interrupt service routines (ISRs) usually causes concurrency bugs. Specifically, when one or more ISRs attempt to preempt a sequence of instructions which are expected to be atomic, a kind of concurrency bugs namely atomicity violation may occur, and it is challenging to find this kind of bugs precisely and efficiently. In this paper, we propose a static approach for detecting atomicity violations in interrupt-driven programs. First, the program model is constructed with interruption points being selected to determine the possibly influenced ISRs. After that, reachability computation is conducted to build up a whole abstract reachability tree, and a delayed ISR-triggering strategy is employed to reduce the state space. Meanwhile, unserializable interleaving patterns are recognized to achieve the goal of atomicity violation detection. The approach has been implemented as a configurable tool namely CPA4AV. Extensive experiments show that CPA4AV is much more precise than the relative tools available with little extra time overhead. In addition, more complex situations can be dealt with CPA4AV.

In Android 6.0 and above, the install-time permission model is replaced with the runtime permission model (RPM), where permission requesting is performed at runtime, rather than at install time, to protect users' privacy. The RPM brings certain benefits to security, but still has drawbacks that are exploitable by malware. The permission could be attained under a reasonable context and then be freely used under another context for executing malicious behavior without notifying users. In addition, the RPM may cause bugs when developers forget to add permission checking before using it. Motivated by this, we propose RTPDroid, an approach to detect implicitly malicious behaviors and bugs brought by the RPM. To do so, implicitly malicious behaviors and bugs are defined formally. Then, notions of user-aware contexts as well as user-aware call graphs are defined and utilized for the detection. Experiments on 221 real-world apps reveal 131 bugs and 174 implicitly malicious behaviors under the RPM.

In Android 6.0 and above, Install-time Permission Model is replaced with Runtime Permission Model (RPM) where permission requesting is performed at runtime, rather than at install-time, to protect users' privacy. RPM brings certain benefits to security, but still has drawbacks that are exploitable by malware. The permission could be attained under a reasonable context and then be freely used under another context for executing malicious behavior without notifying users. In addition, RPM may cause bugs when developers forget to add permission checking before using the permission. Motivated by these problems, we propose RTPDroid, an approach to the detection of implicitly malicious behaviors and bugs brought by RPM. In this approach, these implicitly malicious behaviors and bugs are defined formally. Then, notions of user-aware contexts as well as user-aware call graphs are utilized for the detection. Experiments on 221 real-world apps reveal 131 bugs and 174 implicitly malicious behaviors under RPM.

Certificate validation in Secure Sockets Layer or Transport Layer Security protocol (SSL/TLS) is critical to Internet security. Thus, it is significant to check whether certificate validation in SSL/TLS implementations is correctly implemented. With this motivation, we propose a novel differential testing approach that is based on the standard Request for Comments (RFC). First, rules of certificates are extracted automatically from RFCs. Second, low-level test cases are generated through dynamic symbolic execution. Third, high-level test cases, i.e., certificates, are assembled automatically. Finally, with the assembled certificates being test cases, certificate validations in SSL/TLS implementations are tested to reveal latent vulnerabilities or bugs. Our approach named RFCcert has the following advantages: (1) certificates of RFCcert are discrepancy-targeted, since they are assembled according to standards instead of genetics; (2) with the obtained certificates, RFCcert not only reveals the invalidity of traditional differential testing but also is able to conduct testing that traditional differential testing cannot do; and (3) the supporting tool of RFCcert has been implemented and extensive experiments show that the approach is effective in finding bugs of SSL/TLS implementations. In addition, by providing seed certificates for mutation approaches with RFCcert, the ability of mutation approaches in finding distinct discrepancies is significantly enhanced.

Certificate validation in Secure Socket Layer or Transport Layer Security protocol (SSL/TLS) is critical to Internet security. Thus, it is significant to check whether certificate validation in SSL/TLS is correctly implemented. With this motivation, we propose a novel differential testing approach which is directed by the standard Request For Comments (RFC). First, rules of certificates are extracted automatically from RFCs. Second, low-level test cases are generated through dynamic symbolic execution. Third, high-level test cases, i.e. certificates, are assembled automatically. Finally, with the assembled certificates being test cases, certificate validations in SSL/TLS implementations are tested to reveal latent vulnerabilities or bugs. Our approach named RFCcert has the following advantages: (1) certificates of RFCcert are discrepancy-targeted since they are assembled according to standards instead of genetics; (2) with the obtained certificates, RFCcert not only reveals the invalidity of traditional differential testing but also is able to conduct testing that traditional differential testing cannot do; and (3) the supporting tool of RFCcert has been implemented and extensive experiments show that the approach is effective in finding bugs of SSL/TLS implementations.