We develop CoreScan, a comprehensive formal analysis framework for analyzing the access control mechanism of 5G core networks. In doing so, we build the first comprehensive formal model for the access control mechanism of 5G core network that considers the indirect communication mode and 5G roaming. Given a global property, CoreScan employs the compositional verification technique that leverages the assume-guarantee style reasoning approach to decompose the system model into multiple disjoint components and applies the split assertion principle to identify local assumptions and guarantees. The model's global security property holds if and only if all local guarantees derived from the global property are verified in their respective components. CoreScan features a configurable adversary model, enabling the evaluation of access control properties under diverse adversary capabilities. We tested 61 access control properties with CoreScan and uncovered five new classes of exploitable privilege escalation vulnerabilities in the 5G standards. Additionally, we found that most previously known overprivilege vulnerabilities in direct communication also extend to indirect communication and roaming settings.

We present 5GCVerif, a model-based testing framework designed to formally analyze the access control framework of the 5G Core. With its modular design, 5GCVerif employs various abstraction techniques to craft an abstract model that captures the intricate details of the 5G Core's access control mechanism. This approach offers customizability and extensibility in constructing the abstract model and addresses the state explosion problem in model checking. 5GCVerif also sidesteps the challenge of exhaustively generating models for all possible core network configurations by restricting the model checker to explore policy violations only within the valid network configurations. Using 5GCVerif, we evaluated 55 security properties, leading to the discovery of five new vulnerabilities in 5G Core's access control mechanism. The uncovered vulnerabilities can result in multiple attacks including unauthorized entry to sensitive information, illegitimate access to services, and denial-of-services.

MOTIVATION: Researchers and practitioners use a number of popular sequence comparison tools that use many alignment-based techniques. Due to high time and space complexity and length-related restrictions, researchers often seek alignment-free tools. Recently, some interesting ideas, namely, Minimal Absent Words (MAW) and Relative Absent Words (RAW), have received much interest among the scientific community as distance measures that can give us alignment-free alternatives. This drives us to structure a framework for analysing biological sequences in an alignment-free manner. RESULTS: In this application note, we present Alignment-free Dissimilarity Analysis & Comparison Tool (ADACT), a simple web-based tool that computes the analogy among sequences using a varied number of indexes through the distance matrix, species relation list and phylogenetic tree. This tool basically combines absent word (MAW or RAW) computation, dissimilarity measures, species relationship and thus brings all required software in one platform for the ease of researchers and practitioners alike in the field of bioinformatics. We have also developed a restful API. AVAILABILITY AND IMPLEMENTATION: ADACT has been hosted at http://research.buet.ac.bd/ADACT/. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.