Ying Xie

Formal verification is paramount for neural networks in safety-critical domains yet remains constrained by the trade-off between precision and scalability, especially with modern high frequency activation functions. However, the inherent NP-hardness of the problem forces a fundamental trade-off between scalability and precision in existing methods, which fail to adequately capture the high-frequency nonlinearities of modern activations. To address this, Quadratic Approximation based Verification via Fourier series and Taylor truncation (QAV-FT) is proposed as a framework unifying Fourier-enhanced quadratic approximation and Taylor remainder-aware error control. Specifically: (i) A Fourier-based quadratic abstraction is formulated for arbitrary activations, with a rigorous error bound established via Jackson’s theorem and Lebesgue constant analysis; (ii) A second-order propagation scheme utilizing Lagrange remainder theory is devised to analytically derive sound, tight bounds with reduced symbolic complexity; and (iii) These mechanisms are integrated into a scalable full-network verification algorithm. Empirical results on MNIST-FC and other benchmarks demonstrate that QAV-FT achieves an average certification accuracy of 96.8% across complex activations like Swish, GELU, and Mish, with favorable accuracy and efficiency over comparable methods on partial models.

Intrusion detection systems (IDS) can effectively monitor network traffic and accurately detect malicious behaviors. In Internet of Things (IoT) environments, the massive influx of heterogeneous, resource-constrained devices introduces more complex security challenges, making IDS even more crucial for maintaining network security. However, the presence of redundant or irrelevant features in network traffic can significantly degrade the detection performance of IDS. To address this issue, this paper proposes a Feature distribution and Gini Impurity Filter-based intrusion feature selection method (FGIF). It combines the cardinality and Gini impurity distributions of features within a dataset to construct a multi-parameter evaluation framework, which is used to define efficient feature filtering rules that eliminate redundant and irrelevant features. Theoretical analysis demonstrates that, compared to entropy-based methods, FGIF mitigates selection bias during the feature selection process and significantly reduces computational overhead. Experiments conducted on six widely used IDS benchmark datasets and five commonly adopted classification models further confirm its effectiveness. FGIF significantly reduces feature dimensionality while maintaining detection performance comparable to that of the full feature set. Moreover, compared to existing state-of-the-art methods, FGIF achieves a superior balance between dimensionality reduction and model performance.

Internet of Things (IoT) revolutionizes data collection, especially in e-healthcare, where patients data from wearables and sensors improves medical services. However, IoT’s limitations in computing and storage require cloud outsourcing. Combining IoT with the cloud has potential but raises concerns about data security. Leveraging cloud storage presents an attractive solution for accommodating the substantial volume of data outsourced by IoT devices. As the outsourcing of real-time data to cloud storage becomes commonplace, the adoption of data auditing schemes emerges as a means to ensure data integrity. To curtail operational expenses, various deduplication techniques are commonly employed on outsourced data, effectively sidestepping redundant data and resulting in storage and bandwidth efficiencies. Although real-time data typically remains distinct due to its diverse origins, scenarios such as data sharing or trading in data-driven services and datamarkets can lead to data redundancy. Moreover, in order to fortify against any potential information leakage, encryption is implemented prior to deduplication. Convergent Encryption (CE) stands as a prominent exemplar of this approach. Effectively integrating data auditing, deduplication, and encryption for wireless sensor devices is no trivial task. To efficiently and securely accommodate data while authenticating them through a heterogeneous framework, we present a novel remote data checking scheme, denoted as the VRDC scheme. This scheme empowers IoT data to be encrypted, updated, deduplicated, and audited, aligning with the imperatives of security, privacy, and efficiency. Through comprehensive security analysis, we establish that our VRDC scheme is fortified against potential threats. Our experimental findings highlight the efficiency of our approach in the realms of auditing, deduplication, and updates. Furthermore, the evidence highlights the potential for optimization within our scheme when compared to related works. This is achieved through the careful management of dynamic update scales within a file.

Blockchain is promised for a wide range of applications in fields such as the Internet of Things and cryptocurrencies. Properly utilized, blockchain technology can play a positive role in the social economy. However, there are many gray industries, such as gambling and money laundering, which also build an anonymous blockchain to start illegal acts, and cause negative effects on the economy and society. There has not been any research on detecting anonymous blockchains and discovering nodes that use anonymous blockchains. We propose ChainDetector, a technique for detecting anonymous blockchains using network traffic and discovering nodes that use anonymous blockchains. We exploit the traffic features of blockchain at runtime and use CNN models to train the identification and discovery of blockchain traffic in the network. The results show that we can achieve 96% identification accuracy for some types of blockchain traffic.

Based on the Internet of Behavior (IoB), mobile crowd-sensing (MCS) utilizes the Internet of Things (IoT) to recruit users by analyzing behavioral patterns. MCS is widely used in numerous large-scale and complex monitoring services, but it cannot provide stable and high-quality services due to nondeterministic user mobility and behaviors, which has a vital impact on recruiting high-quality users. In this article, a stochastic semi-algebraic hybrid system (SSAHS) model is constructed to characterize the user mobility and behaviors of the MCS systems. Based on the definition of probabilistic path and task execution rate, a nondeterministic evaluation mechanism is proposed to measure nondeterministic user mobility and behaviors and to give the probability of the user completing the MCS task under the specified time bound and space conditions. The greater the probability is, the higher the quality of the user. Furthermore, a user recruitment scheme based on a nondeterministic evaluation mechanism (NUR) is developed. The NUR employs historical user data to predict user mobility and behaviors; high-quality users are recruited to quickly upload reliable sensing data. We conduct simulation experiments based on a real-world user trace dataset, Geolife.The results show that compared with competing recruitment strategies, NUR achieves a higher quality of service for the same MCS sensing tasks.

With the rapid development of Internet of Things (IoT) in recent years, the security of IoT becomes more and more prominent. To protect data privacy and device availability, identity authentication technology has been applied to the IoT environment. However, although scholars have designed a variety of authentication protocols for the IoT environment, the resource costs of these protocols are still expensive for resource-constrained devices. In particular, when the frequent upgrade of computer hardware has led to a gradual increase in the key length of the cryptosystem, IoT devices are hard to keep up with the upgrade speed because of the balance between cost and tasks. Although the storage space has increased in recent years, the computational and communication capabilities are still limited by some physical factors, such as energy, power, and communication link bandwidth. To improve the situation, this article proposes an anonymous authentication protocol suitable for IoT devices with current hardware performance, which is based on elliptic curve and signcryption techniques. Compared to other protocols, our protocol further reduces the communication and computing cost of the client devices while ensuring security requirements. Thus, we formally prove its theoretical security under the random oracle model and use simulation experiments to verify that the protocol can effectively reduce the resource requirements.

Mobile edge computing provides high computing power, data storage capacity and bandwidth requirements for Internet of Things (IoT) through edge servers that process data close to data sources or users. In practical, mobile edge computing can be used to implement image steganography in IoT. Considering imperceptibility, security and capacity are important indicators for image steganography, this paper propose an image steganography based on evolutionary multi-objective optimization (EMOsteg). The EMOsteg preprocesses the image through a high-pass filters bank to find noise and texture regions that are difficult to model. By perturbing the image on noise and texture regions in multiple directions, the embedded capacity is increased. By defining the imperceptibility and security as an antigen, defining the perturbation positions of the cover image as an antibody, the EMOsteg uses the artificial immune principle to heuristically obtain the perturbation population through feature extraction of the perturbation and adaptive evolution operations. And the Pareto optimal is used to find the optimal perturbation in the last generation population. The simulation experiments analyze the convergence of the algorithm and the diversity of the solutions. In simulation experiments, the MSE, PSNR and SSIM were adopted to evaluate the imperceptibility, and the results show that the MSE value of our algorithm is 0.000308, the PSNR is 82.7501 and the SSIM approaches 1, they are better than comparison algorithms. The average detection error PE under SPA was adopted to detect the security, and the results show that our algorithm is more robust against anti-SPA steganalysis. In order to evaluate the performance of real-time, the embedding time of the same secret under different algorithms were compared, and the results show that our algorithm is faster than comparison algorithms in the terminal. In summary, the proposed algorithm can maintain the image quality while resist steganalysis tools, and realize real-time processing.