PyDejaVu-RV 1.0.0

PyDejaVu is a Python implementation that wraps the original DejaVu jar file, providing a bridge between Python and the Java-based DejaVu runtime verification tool. This wrapper extends DejaVu's functionality by supporting a 2-phase monitoring approach.

PyDejaVu

PyDejaVu is a Python library that wraps the original DejaVu binary, providing a bridge between Python and the Scala-based (and JVM-based) DejaVu runtime verification tool. It is a powerful tool designed for two-phase Runtime Verification (RV) processing, similar to the Tp-DejaVu tool, combining the flexibility and expressiveness of Python with the rigorous, declarative monitoring capabilities of the DejaVu tool.

Two-Phase Runtime Verification

PyDejaVu operates in two distinct phases:

1. Operational Runtime Verification (Phase 1):

   • This phase is implemented in Python, allowing for any Pythonic operations on the events. You can perform arithmetic, string manipulations, and Boolean logic, and leverage Python's extensive data structures and objects for storing data and making complex calculations. This flexibility enables PyDejaVu to handle a wide range of operational tasks during runtime, offering users the ability to customize how events are processed and analyzed.

2. Declarative Monitoring (Phase 2):

   • The second phase is declarative and leverages the DejaVu tool to perform monitoring against a first-order past time temporal logic specification. This phase ensures that the runtime behavior conforms to the formal properties defined in the specification. By integrating with DejaVu, PyDejaVu provides a robust framework for verifying that the system adheres to specified safety properties, making it suitable for applications requiring high levels of assurance.

PyDejaVu Installation

PyDejaVu is a Unix-compatible tool designed for cross-platform use, initially developed on macOS and tested on both macOS and Ubuntu Linux distributions. While specifically tested on these two platforms, PyDejaVu may potentially work on other Unix-like systems as well, though this would require further testing to confirm. It's important to note that as a Unix-based tool, PyDejaVu is not natively compatible with Windows and may require additional setup and modifications, to run on Windows machines.

Here we suggest three methods of installation:

• Pip Installation: For users who need to use PyDejaVu without making changes to the codebase, pip offers a quick and straightforward setup. This method allows you to focus on using the tool rather than managing its dependencies.
• Docker Installation: Docker provides a robust solution for running PyDejaVu in an isolated and consistent environment. This method is ideal for users who prefer not to modify their local system or manage package installations manually. With Docker, you don't need to prepare your system for running PyDejaVu, as the Docker image comes pre-packaged with all the necessary Scala and Java dependencies required for DejaVu.
• Source Code Installation: Installing the source code is a great option if you need more flexibility and control over the PyDejaVu project. Here are some reasons why you might choose this method:
  • Customization and Modification: If you plan to modify the code to suit specific requirements or contribute to the project, installing the source code gives you direct access to all the files. This is ideal for developers who want to extend or alter the functionality of PyDejaVu.
  • Development and Debugging: When working on new features or fixing bugs, having the source code installed locally allows you to test changes immediately. This setup is essential for contributors or developers actively working on the PyDejaVu project.
  • Learning and Exploration: If you're interested in understanding how PyDejaVu works internally, studying the source code can be very educational. You can explore the implementation details, experiment with changes, and see how different components interact.

Pip Installation

👉 Before proceeding, ensure your environment is properly configured according to the instructions in the environment setup guide. This step is crucial for the successful execution of PyDejaVu and helps prevent potential issues arising from an incorrectly set up environment.

Step 1: Create Virtual Environment

Creating a virtual environment is highly recommended when installing PyDejaVu. A virtual environment isolates your project's dependencies from the global Python installation, preventing package conflicts and making dependency management easier.

Create the Virtual Environment:

python3 -m venv pydejavu-env

This command creates a new directory called pydejavu-env containing the isolated Python environment.

Activate the Virtual Environment:

source pydejavu-env/bin/activate

After activation, your command prompt will change to indicate that you are now using the virtual environment.

👉Note: Remember to activate the virtual environment each time you start a new session to ensure you are using the isolated environment.

Step 2: Install PyDejaVu

With the virtual environment activated, install the latest version of PyDejaVu from PyPI:

pip install pydejavu-rv

This command will download and install PyDejaVu along with all its dependencies into your virtual environment.

To upgrade an existing installation to the latest version:

pip install --upgrade pydejavu-rv

Step 3: Verify the Installation

After installation, verify that PyDejaVu has been installed correctly:

pip show pydejavu-rv

This command should display details about the PyDejaVu package, confirming a successful installation within your virtual environment. You should see output similar to:

Name: PyDejaVu-RV
Version: x.y.z
Summary: PyDejaVu is a Python implementation that wraps the original DejaVu jar file, providing a bridge between Python and the Java-based DejaVu runtime verification tool. This wrapper extends DejaVu's functionality by supporting a 2-phase monitoring approach.
Home-page: https://github.com/moraneus/pydejavu
Author: moraneus
Author-email: [e-mail]
License: Apache-2.0
Location: /path/to/your/python/site-packages
Requires: psutil, pyjnius, pytest, pytest-forked, pytest-xdist

Step 4: Operate PyDejaVu

To test the library and explore the capabilities of PyDejaVu, you can download the experiments archive, which contains the experiments used in our paper. This archive includes three folders named example_1, example_2 and example_3, each corresponding to a different experiment. Each example folder contains all the necessary files to run the experiment.

• Extract the experiments.zip file:

  unzip experiments.zip
  

• Change directory to the example folder you wish to run:

  cd example_X
  

  Replace X with the example number (1 to 3).

• Execute the experiment using the provided bash script. Make sure you are execute it from the virtual environment.

  ./run_experiment
  

  In some cases, if run_experiment cannot be run, you need to make it executable using the following command:

  chmod +x run_experiment
  

  This script automates the execution of all experiments within the specified example_X folder. It sequentially runs the experiments using different log files to evaluate PyDejaVu's performance across varying trace sizes (10K, 100K, 500K, and 1M). Upon completion, the results will be saved in a file named result-spec-X.

🛠️ Troubleshooting

If you encounter issues during installation or usage of PyDejaVu, consider the following:

• Python Environment: Ensure your Python environment is correctly configured and you have the necessary permissions to install packages.
• Virtual Environment: If using a virtual environment, activate it before running the pip install command:

  source path/to/your/venv/bin/activate
  

• Dependencies: If you encounter dependency-related issues, try installing them separately

  pip install psutil pyjnius pytest pytest-forked pytest-xdist
  

• Version Conflicts: In case of version conflicts, consider creating a new virtual environment for a clean installation.
• System Requirements: Ensure your system meets the requirements for running Java-based applications, as PyDejaVu relies on a Java runtime.

Docker Installation

The Docker installation process automatically clones the latest PyDejaVu source code inside the container. Unlike the standard installation method, it does not use the pip install pydejavu-rv command. Instead, it builds and installs PyDejaVu directly from the cloned source code within the Docker environment. This approach ensures that you are running the most recent version of PyDejaVu, including the latest features and updates that may not yet be available through PyPI.

Prerequisites

Ensure Docker is installed. You can download Docker from here.

Step 1: Clone the Repository

First, clone the repository to your local machine:

git clone https://github.com/moraneus/pydejavu.git
cd pydejavu

Step 2: Build the Docker Image

Ensure the Docker service is running, then build the image:

docker build -t pydejavu .

This command creates a Docker image named "pydejavu" (based on a Dockerfile located in the root project folder) with the following features:

• Ubuntu based environment for running PyDejaVu.
• Java and Scala installations.
• Python with Poetry for dependency management.
• PyDejaVu and its dependencies.
• Linter and tests run to ensure proper configuration.

You should see output similar to:

[+] Building 412.7s (17/17) FINISHED                                                                                                                                                                        
 => [internal] load build definition from Dockerfile                                                                                                                                                   0.0s
 => => transferring dockerfile: 2.32kB                                                                                                                                                                 0.0s
 => [internal] load .dockerignore                                                                                                                                                                      0.0s
 => => transferring context: 2B                                                                                                                                                                        0.0s
 => [internal] load metadata for docker.io/library/python:3.12-slim                                                                                                                                    2.6s
 => [ 1/13] FROM docker.io/library/python:3.12-slim@sha256:XXXchecksumXXX                                                                           57.4s
 => => resolve docker.io/library/python:3.12-slim@sha256:XXXchecksumXXX                                                                              0.0s
 => => sha256:XXXchecksumXXX 9.12kB / 9.12kB                                                                                                         0.0s
 => => sha256:XXXchecksumXXX 1.75kB / 1.75kB                                                                                                         0.0s
 => => sha256:XXXchecksumXXX 5.11kB / 5.11kB                                                                                                         0.0s
 => => sha256:XXXchecksumXXX 29.16MB / 29.16MB                                                                                                       6.1s
 => => sha256:XXXchecksumXXX 3.33MB / 3.33MB                                                                                                         0.8s
 => => sha256:XXXchecksumXXX 13.38MB / 13.38MB                                                                                                      57.1s
 => => sha256:XXXchecksumXXX 250B / 250B                                                                                                             1.2s
 => => extracting sha256:XXXchecksumXXX                                                                                                              0.5s
 => => extracting sha256:XXXchecksumXXX                                                                                                              0.1s
 => => extracting sha256:XXXchecksumXXX                                                                                                              0.3s
 => => extracting sha256:XXXchecksumXXX                                                                                                              0.0s
 => [ 2/13] RUN apt-get update && apt-get install -y     curl     wget     gnupg2     software-properties-common     unzip     zip     && rm -rf /var/lib/apt/lists/*                                 21.8s
 => [ 3/13] RUN wget -O- https://packages.adoptium.net/artifactory/api/gpg/key/public | tee /usr/share/keyrings/adoptium.asc     && echo "deb [signed-by=/usr/share/keyrings/adoptium.asc] https://  179.2s
 => [ 4/13] RUN curl -s "https://get.sdkman.io" | bash     && bash -c "source $HOME/.sdkman/bin/sdkman-init.sh && sdk install scala 2.12.18"                                                          14.6s 
 => [ 5/13] RUN bash -c "source $HOME/.sdkman/bin/sdkman-init.sh && scalac -version && java -version && python --version"                                                                              0.6s 
 => [ 6/13] RUN pip install --no-cache-dir "poetry==1.6.1"                                                                                                                                            18.4s 
 => [ 7/13] RUN poetry config virtualenvs.create false                                                                                                                                                 0.5s 
 => [ 8/13] RUN pip install flake8                                                                                                                                                                     2.5s 
 => [ 9/13] RUN git clone https://github.com/moraneus/pydejavu.git /app                                                                                                                               20.1s 
 => [10/13] WORKDIR /app                                                                                                                                                                               0.0s 
 => [11/13] RUN poetry install --no-interaction --no-ansi                                                                                                                                              2.2s 
 => [12/13] RUN bash -c "source $HOME/.sdkman/bin/sdkman-init.sh && flake8 . --count --select=E9,F63,F7,F82 --show-source --statistics && flake8 . --count --exit-zero --max-complexity=10 --max-line  0.7s 
 => [13/13] RUN bash -c "source $HOME/.sdkman/bin/sdkman-init.sh && pytest --forked"                                                                                                                  90.6s 
 => exporting to image                                                                                                                                                                                 1.4s 
 => => exporting layers                                                                                                                                                                                1.4s 
 => => writing image sha256:XXXchecksumXXX                                                                                                           0.0s 
 => => naming to docker.io/library/pydejavu     

Step 3: Run the Docker Container

Start an interactive session in the Docker container:

docker run -it pydejavu

This command starts an interactive session inside the Docker container, where PyDejaVu is set up and ready to use.

Step 4: Operate PyDejaVu

Inside the Docker container, you can use PyDejaVu with no addition configuration. For example:

Example: Running a Pre-defined Monitor

cd /app/examples/pydejavu_monitor
python monitor_for_detecting_suspicious_login_patterns.py

Example: Using the CLI

cd /app/examples/cli
python -m pydejavu --bits 20 --stats true --qtl sample.qtl --operational sample.pqtl --trace sample.log

Example: Experiments

Since we are using the PyDejaVu source code inside the Docker container we have direct access to the experiment folders.

• Change directory to the experiment folder you wish to test:

  cd /app/experiments/example_X
  

  Replace X with the example number (1 to 3).

• Execute the experiments using the provided bash script:

  bash -i run_experiment
  

This script automates the execution of all experiments within the specified example_X folder. It sequentially runs the experiments using different log files to evaluate PyDejaVu's performance across varying trace sizes (10K, 100K, 500K, and 1M). Upon completion, the results will be saved in a file named result-spec-X.

🛠️ Troubleshooting

• Docker Service: Ensure the Docker service is running before building or running containers.

• Persistent Storage: To persist data between container runs and share files between your host machine and the Docker container, you can use Docker volumes. This is particularly useful when you have predefined PyDejaVu monitor files or other resources on your local machine that you want to use inside the container without copying or rewriting them:

  docker run -it -v /path/on/host:/path/in/container pydejavu
  

• Resource Allocation: If PyDejaVu requires more resources, allocate them using Docker's resource flags:

  docker run -it --cpus 2 --memory 4g pydejavu
  

• Cached Images: If the Docker build command completes unusually quickly (within a few seconds), it's likely using cached images from previous builds. In this case, you may need to remove the older Docker containers and images associated with your project (in this case, pydejavu) to force a fresh build. Here's how you can do this:

  1. Stop and remove existing containers:

     docker stop $(docker ps -a -q --filter ancestor=pydejavu)
     docker rm $(docker ps -a -q --filter ancestor=pydejavu)
     

  2. Remove associated images:

     docker rmi $(docker images | grep pydejavu | awk '{print $3}')
     

  3. Rebuild your Docker image:

     docker build --no-cache -t pydejavu .
     

  This process ensures that your next build will create a fresh image without relying on potentially outdated cached layers.

• Debugging: To debug issues, you can start a shell in the container:

  docker run -it pydejavu /bin/bash
  

Source Code Installation

👉 Before proceeding, ensure your environment is properly configured according to the instructions in the environment setup guide. This step is crucial for the successful execution of PyDejaVu and helps prevent potential issues arising from an incorrectly set up environment.

Step 1: Clone the Repository

First, clone the repository to your local machine:

git clone https://github.com/moraneus/pydejavu.git
cd pydejavu

Step 2: Install Poetry

This project uses Poetry for managing dependencies and packaging. Follow these steps to set up your development environment:

1. Create and activate a virtual environment:

   python3 -m venv pydejavu-env
   source pydejavu-env/bin/activate
   

2. Install Poetry:

   pip install poetry
   

3. Verify the installation:

   poetry --version
   

   If Poetry is correctly installed, you should see the version number.

Step 3: Install Project Dependencies

With Poetry installed, you can now install the project dependencies. Run the following command in the root directory of the project:

poetry install

This will create a poetry.lock file and install all necessary dependencies for the project.

Step 4: Operate PyDejaVu

After the installation is finished we can use PyDejaVu with no addition configuration.

Example: Running a Pre-defined Monitor

👉Note: Make sure you are in the root directory of PyDejaVu.

cd examples/pydejavu_monitor
python monitor_for_detecting_suspicious_login_patterns.py

Example: Using the CLI

👉Note: Make sure you are in the root directory of PyDejaVu.

cd /app/examples/cli
python -m pydejavu --bits 20 --stats true --qtl sample.qtl --operational sample.pqtl --trace sample.log

Example: Experiments

Since we are using the PyDejaVu source code we have direct access to the experiment folders.

👉Note: Make sure you are in the root directory of PyDejaVu.

• Change directory to the experiment folder you wish to test:

  cd experiments/example_X
  

  Replace X with the example number (1 to 3).

• Execute the experiments using the provided bash script:

  ./run_experiment
  

This script automates the execution of all experiments within the specified example_X folder. It sequentially runs the experiments using different log files to evaluate PyDejaVu's performance across varying trace sizes (10K, 100K, 500K, and 1M). Upon completion, the results will be saved in a file named result-spec-X.

🛠️ Troubleshooting

If you encounter issues during installation or while running the project, consider the following:

• Ensure that your Python version meets the minimum requirement.
• Check that Poetry is correctly installed and accessible from your command line.
• Verify that all dependencies are properly installed by running poetry show.

Usage

In this section, we present a simple usage of the tool divided into two examples. The first example demonstrates how users can easily operate DejaVu directly from PyDejaVu. The second example builds upon the first, showing how to enhance the expressiveness of your application by leveraging the power of PyDejaVu. By leverages DejaVu's capabilities, PyDejaVu involves a few steps before it starts the evaluation process. First, it analyzes and parses the specification to ensure it meets the syntax of QTL (Quantified Temporal Logic). Then, it compiles a Scala-based monitor. This Scala compilation step may take some time, so don't be alarmed if there is a delay during this process. For more advanced usage and explanations, please refer to the documentation.

Example 1

Consider a simple filesystem mechanism that handles several key events. The filesystem allows opening a file with the an open(F, f, m, s), carrying as arguments the folder name F, the filename f (technically a file id), the access mode m (read or write), and the size s which is the maximal number of bytes that can be written. The close(f) event indicates that a file f has been closed. The write event write(f, d) contains the filename and the data d (a string) being written. Additionally, the system supports create(F) and delete(F) events, which represent the creation or deletion of a folder. The requirement we are verifying states that if data is written to a file, the file must have been opened in write mode, not closed since, and must reside in a folder that has been created and not deleted since.

from pydejavu.core.monitor import Monitor

specification = """
prop example: forall f . forall d . 
   write(f, d) ->
     (exists F . Exists s . 
       ((!close(f) S open(F, f, "w", s)) & (!delete(F) S create(F))))
"""

monitor = Monitor(specification)

events = [ 
    {"name": "create", "args": ["tmp"]}, 
    {"name": "open", "args": ["tmp", "f1", "w", "5"]},
    {"name": "write", "args": ["f1", "some text"]},
    {"name": "close", "args": ["f1"]},
    {"name": "delete", "args": ["tmp"]}
]

for e in events:
    monitor.verify(e)
monitor.end()

This code snippet demonstrates how to operate DejaVu directly from PyDejaVu to perform runtime verification based on a formal specification written in first-order past time temporal logic. First, the Monitor class is imported from pydejavu.core.monitor, and the specification, named as example, is defined as a multi-line string. The monitor is then initialized with this specification, setting up the verification environment. A list of events is created to simulate a sequence of I/O operations: creating a folder (create), opening a file (open), writing to it (write), closing it (close), and finally deleting the hosting folder (delete). Each event is a dictionary containing the event name and its arguments. The events are processed in a loop where each event is passed to the monitor.verify(e) method. In this case, where no event handlers are defined, the events are forwarded directly to the declarative phase for verification against the specification. After all events are processed, monitor.end() is called to finalize the evaluation. This step is crucial for obtaining statistics results and for the monitor to release resources appropriately.

Example 1 Output

As shown in the following output snippet, this example reports no errors.

0 errors detected!

==================
  Event Counts:
------------------
  create : 1
  open   : 1
  delete : 1
  close  : 1
  write  : 1
==================

- Garbage collector was not activated

Example 2

from pydejavu.core.monitor import Monitor, event

specification = """
prop example: forall f . 
  !write(f, "false") & (write(f, "true") ->
    (exists F . ((!close(f) S open(F, f, "w")) & (!delete(F) S create(F)))))
"""
monitor = Monitor(specification)
total_sizes: dict[str, int] = {}

@event("open")
def open(F: str, f: str, m: str, s: int):
    global total_sizes
    if m == "w":
        total_sizes[f] = s
    return ["open", F, f, m]

@event("close")
def close(f: str):
    global total_sizes
    del total_sizes[f]
    return ["close", f]

@event("write")
def write(f: str, d: str):
    global total_sizes
    if f not in total_sizes:
        total_sizes[f] = 0
    data_len = len(d)
    ok = total_sizes[f] >= data_len
    if ok:
        total_sizes[f] -= data_len
    return ["write", f, ok]

events = [ 
    {"name": "create", "args": ["tmp"]}, 
    {"name": "open", "args": ["tmp", "f1", "w", "5"]},
    {"name": "write", "args": ["f1", "some text"]},
    {"name": "close", "args": ["f1"]},
    {"name": "delete", "args": ["tmp"]}
]

for e in events:
    monitor.verify(e)
monitor.end()

This code differs from the previous example by incorporating operational event handlers that perform real-time computations and state management before events are passed to the declarative phase for verification. In the earlier code, events were directly forwarded to the declarative phase without any operational processing. Here, the @event decorator is used to define custom handlers for the open, close, and write events, enabling the code to maintain and manipulate state during the operational phase. Generally, the handlers are decorated with the @event("event_name") decorator, linking them to specific events in your specification. This definition is optional; if no handler is defined for a specific event, PyDejaVu will forward the event directly to DejaVu for evaluation. Without any handler definitions, PyDejaVu functions the same as DejaVu without the operational phase.

A key difference is the introduction of the total_sizes dictionary, which tracks the remaining allowed write sizes for each file. In the open handler, the code checks if the file is opened in write mode "w" and initializes the total allowed size s for that file in the total_sizes dictionary. The write handler then uses this information to ensure that the length of the data being written does not exceed the remaining allowed size. It calculates the length of the data d, compares it against the remaining size for the file, and updates the total_sizes accordingly. If the write operation exceeds the allowed size, an ok flag is set to False, indicating that the write is not permitted.

These operational event handlers allow for immediate enforcement of constraints and preliminary checks before events are evaluated against the formal specification in the declarative phase. By performing these computations upfront, the code can prevent invalid or undesirable events from proceeding further, enhancing efficiency and providing immediate feedback. This integration of operational logic with declarative specifications showcases how PyDejaVu increases the expressiveness of the system, enabling more complex and nuanced runtime verification scenarios compared to the previous example where such operational checks were absent.

Example 2 Output

As shown in the following output snippet, this example reports one error because it failed when attempting to write the "some text" string into f1, which is limited to 5 characters.

1 errors detected!

==================
  Event Counts:
------------------
  create : 1
  open   : 1
  delete : 1
  close  : 1
  write  : 1
==================

- Garbage collector was not activated

More Usage Examples

You can find more comprehensive usage examples of monitors in the examples folder and the experiments folder. These folders contain various use cases and demonstrations of how to effectively use PyDejaVu for runtime verification.

Output Files

After each execution of PyDejaVu, several output files are generated and stored in designated folders. These outputs are crucial for reviewing the results of the verification process and understanding the internal workings of the tool.

Logs Folder:

The logs folder will contain the log file from the last execution. This log file is named with a timestamp to ensure that each run's output is distinct and easy to identify.

Output Folder:

The output folder contains several important files generated during the verification process:

• ast.dot: A Graphviz source file used to create an abstract syntax tree (AST) graph for the specification. This file can be visualized using Graphviz to better understand the structure of the specification.
• TraceMonitor.jar: If the specification was compiled into a Java archive, this file will contain the compiled monitor.
• TraceMonitor.scala: If the specification was synthesized into Scala code, this file will be generated. It represents the synthesized monitor in Scala.
• resultFile: This file is primarily used in unit testing to compare the expected errors with the actual errors encountered. It contains the results of the original DejaVu execution, capturing any errors from the verification process. When an error occurs, the event index is written to this file. However, be aware that the resultFile remains empty if no errors are detected during verification. To ensure the resultFile is created correctly, make sure to run monitor.end() to notify DejaVu to close the result file and finalize the execution.
• generated_trace.py (Optional): This file is automatically generated when the user utilizes the CLI options. In this case, a PyDejaVu script is created in the working directory, tailored to the user's input parameters for runtime verification.

These output files provide a comprehensive overview of each execution, allowing you to analyze and debug the behavior of your specifications in detail.

output/
├── ast.dot
├── TraceMonitor.jar
├── TraceMonitor.scala
├── resultFile
└── generated_trace.py  (Optional)

Contributors - For PyDejaVu (Ordered by last name):

• Klaus Havelund, Jet Propulsion Laboratory/NASA, USA
• Moran Omer, Bar Ilan University, Israel
• Doron Peled, Bar Ilan University, Israel