MP-Basset – Systems & Security Group (SSG)

Static POR of Message-Passing Protocols.

MP-Basset is a model checker for message-passing systems. It extends the Basset model checker with quorum transitions, i.e., atomic events consuming multiple messages. MP-Basset supports Partial-Order Reduction (POR) for better scalability of model checking complex message-passing protocols.

News

Release of MP-Basset extension with new optimization called Decompasition-Based Stateful Search (DBBS). The optimization consists of the following features:

Selective push-on-stack for time-efficient backtracking.
Selective hashing for more efficient state matching.
New JPF core version (6.0).

The source code of DBSS/MP-Basset is available for download.

Documentations

MP-Basset supports dynamic Partial-Order Reductions (POR) via Basset, and implements a new static POR algorithm called Local POR (LPOR) [2]. Die new version of MP-Basset also supports MP-State, which is an improvement of explicit-state software model checking of message passing programs.

A short user guide of MP-Basset can be found in [1].

[1]

Péter Bokor, Johannes Kinder, Marco Serafini and Neeraj Suri, “Efficient Model Checking of Fault-Tolerant Distributed Protocols”, Proc. of the IEEE Int’l Conf. on Dependable Systems and Networks (DSN-DCCS), 2011

[2]

Péter Bokor, Johannes Kinder, Marco Serafini and Neeraj Suri, “Supporting Domain-Specific State Space Reductions through Local Partial-Order Reduction”, Proc. of the 26th IEEE/ACM Int’l Conf. on Automated Software Engineering (ASE), pp. 113-122, 20111.

Download & Installation

The complete source code of MP-Basset is available here. The new version of MP-Basset is integrated with the latest JPF core and includes our new technique MP-State.

MP-Basset includes Java Pathfinder (the model checker engine utilized by Basset, and, in turn, MP-Basset) and a Java-based open library implementation of LPOR.

MP-Basset can be installed similar to Basset.

MP-Basset runs from the command line. You can run your first MP-Basset application using the following simple script (MPBasset).

For example, the following command starts MP-Basset with LPOR for the model of the Paxos consensus protocol with 3 acceptor processes.

./MPbasset +fw.mp=1 +fw.spor=1 paxos.actor.DriverMP 3

Examples

Example message-passing protocols written in MP, the input language of MP-Basset, can be found in the MP-Basset distribution (/jpf-actor/src/examples/).

The following examples are available:

Paxos consensus: /jpf-actor/src/examples/paxos/
Echo multicast: /jpf-actor/src/examples/multicast/
Regular register: /jpf-actor/src/examples/register/
Zab atomic broadcast: /jpf-actor/src/examples/zab/

News & Events
IEEE TFS’24 Y. Li et al, Adversarial Attack Detection via Fuzzy Predictions. pdf
ECCV’24 Y. Li et al, Self-Supervised Representation Learning for Adversarial Attack Detection. pdf
ANRW '24 S. Kastanakis et al, Investigating Location-Aware Advertisements in Anycast IP Networks. pdf
IJCNN '24 Y. Li et al, Rethinking Self-Supervised Learning for Cross-Domain Adversarial Sample Recovery. pdf
ICANN '24 Y. Li et al, Federated Adversarial Learning for Robust Autonomous Landing Runway Detection. pdf
IJCNN '24 A. Pellcier et al, UNICAD: A Unified Approach for Attack Detection, Noise Reduction and Novel Class Identification. pdf
NFM '24 O. Gunasekera et al, Real Arithmetic in TLAPM. pdf
IEEE TCC S. Manzoor et al, Enabling Multi-Layer Threat Analysis in Dynamic Cloud Environments. pdf
arXiv S. Winter et al, Error Propagation Analysis for Multithreaded Programs: An Empirical Approach. pdf
Springer Open’24 E. Chuah et al, An Empirical Study of Reflection Attacks Using NetFlow Data. pdf
Space Policy’23 V. Varadharajan et al, Security Challenges When Space Merges With Cyberspace. pdf
LANMAN’23 S. Rene et al, Scalable Content-centric Routing for Hybrid ICN. pdf
DAPPS’23 N. Keizer et al, Ditto: Towards Decentralised Similarity Search for Web3 Services. pdf
IMC’23 L. Balduf et al, The Cloud Strikes Back: Investigating the Decentralization of IPFS. pdf
CAMLIS’23 S. Trawicki et al, Compilation as a Defense: Enhancing DL Model Attack Robustness via Tensor Optimization. pdf
CAMLIS’23 L. Birch et al, Model Leeching: An Extraction Attack Targeting LLMs. pdf
SSCI’23 Y. Li et al, Fuzzy Detectors Against Adversarial Attacks. pdf
IMC’23 S. Kastanakis et al, 20 Years of Inferring Inter-domain Routing Policies. pdf
DASC’23 B. Yuksek et al, Federated Meta Learning for Visual Navigation in GPS-denied Urban Airspace. pdf
NDSS’24 S. Sridhar et al, Content Censorship in the InterPlanetary File System. pdf
MASS’23 Z. Yu et al, RAFL: A Robust and Adaptive Federated Meta-Learning Framework Against Adversaries. pdf
TOPS’23 Y. Lu et al, Privacy-preserving Decentralized Federated Learning over Time-varying Communication Graph. pdf
T-ASE’23 Y. Lu et al, Transactive Energy System Deployment over Insecure Communication Links. pdf
IJCNN’23 Y. Li et al, Domain Generalization and Feature Fusion for Cross-domain Imperceptible Adversarial Attack Detection. pdf
CyBok: SSG Prof. Suri defines NCSC’s CyBOK knowledge area on Distributed Systems Security
Prof. Suri to lead LU's ACE-CSE
Security Institute to lead £3M UKRI-TAS research node to examine cybersecurity in autonomous systems.^New
MSN'22 Best Paper Award for Z. Yu et al, PPFM: An Adaptive and Hierarchical Peer-to-Peer Federated Meta-Learning Framework
ICNC '23: A. Taha et al, Cloud Security Requirement Based Threat Analysis, to appear.
MSN'22: Z. Yu et al, PPFM: An Adaptive and Hierarchical Peer-to-Peer Federated Meta-Learning Framework. pdf
CIDUE/SSCI'22: E. Soares et al, Similarity-based Deep Neural Network to Detect Imperceptible Adversarial Attacks. pdf
ISSRE'22: Y. Chen et al, SlowCoach: Mutating Code to Simulate Performance Bugs. pdf
FGCS'22: M. Bradbury et al, Information Management for Trust Computation on Resource-constrained IoT Devices. pdf
ToSN'22: M. Bradbury et al, Threat Modelling Guided Trust-based Task Offloading for Resource-constrained Internet of Things. pdf
NCA'21: E. Chuah et al, Challenges in Identifying Network Attacks Using Netflow Data. pdf
COSE'21: B. Green et al, PCaaD: Towards automated determination and exploitation of industrial systems. pdf