Android apps communicate with each other through a mechanism called Inter-Process Communication (IPC) that allows them to exchange messages known as intents. IPC uses Mandatory Access Control (MAC), referred to as an Intent Firewall, to protect and manage intents between apps. However, IPC poses a significant risk, as malicious apps can exploit IPC to attack other apps. This vulnerability arises from the security architecture and implementation inherent to the Android operating system. To mitigate this vulnerability, we have implemented NIST Next Generation Access Control (NGAC) on top of the Intent Firewall to strengthen the enforcement of IPC access control. The NGAC module enforces stricter IPC security policies by using app attributes, including the installation source, app signature, and app type. We tested the NGAC module on Android 13 across various apps, and we evaluated its performance to ensure that the time required to verify intents between apps remains efficient. The results show that the NGAC module is effective and efficient in securing Android IPC.

We study the safety problem for the next-generation access control (NGAC) model. We show that under mild assumptions it is coNP-complete, and under further realistic assumptions we give an algorithm for the safety problem that significantly outperforms naive brute force search. We also show that real-world examples of mutually exclusive attributes lead to nearly worst-case behavior of our algorithm.

The increasing growth of threats to Industrial Control Systems (ICS) in the energy sector puts this critical infrastructure at high risk. Consequently, holistic approaches are needed to assess the criticality of ICS assets, identify relevant security threats, and develop mitigation techniques to make the energy critical infrastructure cyber-resilient. This paper presents a methodology for analyzing the criticality and resiliency of ICS assets by assessing the impact caused by attacks on such assets. Our approach consists of modeling the ICS architecture in a form that is suitable for analysis. We use Coloured Petri Nets (CPN) for formal representation and analysis – CPN is supported by automated tools for analysis and it has been used for verification of real-world systems. We use Spoofing, Tampering, Repudiation, Information Disclosure, Denial of Service, and Elevation of Privilege (STRIDE) for evaluating the threats in the ICS architecture. We use Microsoft Threat Modeling Tool (MTMT) for ICS threat modeling that classifies the threats into the categories defined in STRIDE. Based on the type of threat on each asset and its impact on the entire ICS, we rank the asset’s criticality. The threat modeling framework assesses the criticality and resiliency of tangible and intangible assets, thus addressing the gap in the current research. Threat models are also converted into CPN models. The CPN models of the ICS architecture and the threat model are then composed. The methodology then verifies the resulting CPN. This verification explores the system states where the ICS cannot resist the attacks and identifies the ICS’s critical assets that have been compromised. The methodology is applied to a wind farm system comprising many distributed subsystems connected via various networks. The result shows that the methodology is practical for the ICS verification and assets criticality assessment, providing recommended mitigations to construct a robust ICS.

Access control policies (ACPs) are natural language statements that describe criteria under which users can access resources. We focus on constructing NIST Next Generation Access Control (NGAC) ABAC model from ACP statements. NGAC is more complex than RBAC or XACML ABAC as it supports dynamic, event-based policies, as well as prohibitions. We provide algorithms that use spaCy, a NLP library, to extract entities and relations from ACP sentences and convert them into the NGAC model. We then convert this NGAC model into Neo4j representation for the purpose of analysis. We apply the approach to various real-world ACP datasets to demonstrate the feasibility and assess scalability. We demonstrate that the approach is scalable and effectively extracts the NGAC ABAC model from large ACP datasets. We also show that redundancies and inconsistencies of ACP sentences are often found in unclean datasets.

This paper describes a model-based test generation approach for testing Urban Search and Rescue (USAR) robots interacting with their environment (i.e., world). Unlike other approaches that assume a static world with attributes and values, we present and test a dynamic world. We use Petri Nets to illustrate a world model that describes behaviors of environmental entities (i.e., actors). The Abstract World Behavioral Test Cases (AWBTCs) are generated by covering the active world model using graph coverage criteria. We also select test-data by input-space partitioning to transform the generated AWBTCs into executable test cases. Reachability of the active world model and efficiency of coverage criteria are also discussed.

This paper describes a model-based test generation approach for testing autonomous systems interacting with their environment (i.e., world). Unlike other approaches that assume a static world with attributes and values, we present and test the world dynamically. We build the world model in two steps: a structural model that constructs environmental factors (i.e., actors) and a behavioral model that describes actors' behaviors over a certain landscape (i.e., snippet). Abstract world behavioral test cases (AWBTCs) are then generated by covering the behavioral model using graph coverage criteria. The world model-based test generation technique (WMBTG) is used on an autonomous ground vehicle (AGV).