docs: add policy related docs and improve examples

docs/source/_static/examples/micronaut-projects/micronaut-core/policies/micronaut-core.cue

@@ -0,0 +1,11 @@
+{
+    target: "micronaut-projects/micronaut-core",
+    predicate: {
+        invocation: {
+            configSource: {
+                uri: =~"^git\\+https://github.com/micronaut-projects/micronaut-core@refs/tags/v[0-9]+.[0-9]+.[0-9]+$"
+                entryPoint: ".github/workflows/release.yml"
+            }
+        }
+    }
+}

docs/source/_static/examples/oracle-quickstart/oci-micronaut/policies/oci-micronaut.dl

@@ -0,0 +1,49 @@
+/* Copyright (c) 2023 - 2023, Oracle and/or its affiliates. All rights reserved. */
+/* Licensed under the Universal Permissive License v 1.0 as shown at https://oss.oracle.com/licenses/upl/. */
+
+
+#include "prelude.dl"
+
+/**
+ *  This is an example policy for OCI Micronaut project.
+ *  See: https://github.com/oracle-quickstart/oci-micronaut
+ */
+
+Policy("oci_micronaut_dependencies", parent, "") :-
+    check_passed(parent, "mcn_build_service_1"),
+    !violating_dependencies(parent, "mcn_build_service_1"), // There should not be any violating dependencies.
+    verify_provenance(dependency, "micronaut-projects/micronaut-core").
+
+// Projects that violate an expected check result.
+.decl violating_dependencies(parent: number, property: symbol)
+violating_dependencies(parent, property) :-
+    is_check(property),
+    transitive_dependency(parent, dependency), // note that since macaron by default does not traverse
+                                               // to transitive, dependencies, in most cases this is
+                                               // identical to `dependency(parent, repo)`.
+    !check_passed(dependency, property),
+    !exception_dependencies(dependency).
+
+// Exceptions for violating dependencies.
+.decl exception_dependencies(dependency: number)
+exception_dependencies(dependency) :-
+    is_repo(dependency, "mapstruct/mapstruct").
+
+exception_dependencies(dependency) :-
+    is_repo(dependency, "mysql/mysql-connector-j").
+
+exception_dependencies(dependency) :-
+    is_repo(dependency, "aws/aws-msk-iam-auth").
+
+exception_dependencies(dependency) :-
+    is_repo(dependency, "h2database/h2database").
+
+// Projects that we expect to generate a provenance.
+.decl verify_provenance(repo_num: number, repo_name: symbol)
+verify_provenance(repo_num, repo_name) :-
+    is_repo(repo_num, repo_name),
+    check_passed(repo_num, "mcn_provenance_level_three_1"),
+    check_passed(repo_num, "mcn_provenance_expectation_1").
+
+// Apply the policy.
+apply_policy_to("oci_micronaut_dependencies", repo) :- is_repo(repo, "oracle-quickstart/oci-micronaut").

docs/source/index.rst

@@ -1,9 +1,89 @@
 .. Copyright (c) 2022 - 2023, Oracle and/or its affiliates. All rights reserved.
 .. Licensed under the Universal Permissive License v 1.0 as shown at https://oss.oracle.com/licenses/upl/.
 
+.. _index:
+
+.. meta::
+   :description: macaron - A CI/CD security analysis tool for supply-chain attacks
+   :keywords: CI/CD, SLSA, supply-chain security
+
+=====================
 Macaron documentation
 =====================
 
+Software supply-chain attacks are becoming more prevalent as the systems get more complex, particularly with respect to the use of open-source
+third-party code. Attacks include stealing credentials, tampering with the
+code, tampering with the code repository, and tampering with the build system.
+It is crucial to have guarantees that the third-party code we rely on is the
+code we expect.
+
+To tackle these problems, `Supply-chain Levels for Software Artifacts (SLSA or "salsa") <https://slsa.dev>`_ is created to improve the integrity and
+protection of the software supply-chain. Macaron can analyze a software
+repository to determine its SLSA level and provide supply-chain transparency of the build process.
+
+--------
+Overview
+--------
+
+Macaron is an analysis tool which focuses on the build process for an artifact and its dependencies. As the SLSA requirements
+are at a high-level, Macaron first defines these requirements as specific
+concrete rules that can be checked automatically. Macaron has a customizable checker platform that makes it easy to define checks that depend on each other.
+
+-------------------------
+Current checks in Macaron
+-------------------------
+
+The table below shows the current set of actionable checks derived from
+the requirements that are currently supported by Macaron.
+
+.. note:: The current checks are designed based on `SLSA v0.1 <https://slsa.dev/spec/v0.1/>`_. Support for `SLSA v1.0 <https://slsa.dev/spec/v1.0/>`_ is currently under development.
+
+.. list-table:: Mapping SLSA requirements to Macaron checks
+   :widths: 20 40 40
+   :header-rows: 1
+
+   * - SLSA level
+     - SLSA spec v0.1
+     - Concrete check
+   * - 1
+     - **Scripted build** - All build steps were fully defined in a “build script”.
+     - Identify and validate build script(s).
+   * - 1
+     - **Provenance available** - The provenance is available.
+     - Check for existence of SLSA provenance. If there are no SLSA provenance, the repo can still be compliant to level 1 given the build script is available.
+   * - 2
+     - **Build service** - All build steps are run using some build service (e.g. GitHub Actions)
+     - Identify and validate the CI service(s) used for the build process.
+   * - 3
+     - **Trusted builders** - Guarantees the identification of the top-level build configuration used to initiate the build. The build is verified to be hermetic, isolated, parameterless, and executed in an ephemeral environment.
+     - Identify and validate that the builder used in the CI pipeline is a trusted one.
+   * - 3
+     - **Build as code** - If a trusted builder is not present, this requirement determines that the build definition and configuration executed by the build service is verifiably derived from text file definitions stored in a version control system.
+     - Identify and validate the CI service(s) used to build and deploy/publish an artifact.
+   * - 3
+     - **Provenance Level three** - Check whether the target has SLSA provenance level 3.
+     - Use the `slsa-verifier <https://github.com/slsa-framework/slsa-verifier>`_ to attest to the subjects in the SLSA provenance that accompanies an artifact.
+   * - 3
+     - **Provenance expectation** - Check if the provenance meets an expectation.
+     - The user can provide an expectation for the provenance as a CUE policy, which will be compared against the SLSA provenance.
+
+----------------------
+How does Macaron work?
+----------------------
+
+.. _fig_macaron:
+
+.. figure:: _static/images/macaron_infrastructure.png
+   :alt: Macaron infrastructure
+   :align: center
+
+   Macaron's infrastucture
+
+Macaron is designed based on a Zero Trust model. It analyzes a target repository as an external
+tool and requires minimal configurations. After cloning a repository, Macaron parses the CI
+configuration files and bash scripts that are triggered by the CI, creates call graphs and other
+intermediate representations as abstractions. Using such abstractions, Macaron implements concrete checks based on a security specification and verifies the desired properties.
+
 .. toctree::
    :maxdepth: 1
 

docs/source/pages/using.rst

@@ -9,6 +9,8 @@ Using Macaron
 
 .. note:: The instructions below assume that you have setup you environment correctly to run Macaron (if not, please refer to :ref:`Installation Guide <installation-guide>`).
 
+.. _analyze-action:
+
 ------------------------------------
 Analyzing a public Github repository
 ------------------------------------
@@ -50,13 +52,45 @@ With the example above, the generated output reports can be seen here:
 - `micronaut-core.html <../_static/examples/micronaut-projects/micronaut-core/analyze_with_repo_path/micronaut-core.html>`__
 - `micronaut-core.json <../_static/examples/micronaut-projects/micronaut-core/analyze_with_repo_path/micronaut-core.json>`__
 
+-------------------------------------------------
+Verifying provenance expectations in CUE language
+-------------------------------------------------
+
+When a project generates SLSA provenances, you can add a build expectation in the form of a
+`Configure Unify Execute (CUE) <https://cuelang.org/>`_ policy to check the content of provenances. For instance, the expectation
+can specify the accepted GitHub Actions workflows that trigger a build, which can prevent using artifacts built from attackers
+workflows.
+
+.. code-block:: shell
+
+  ./run_macaron.sh analyze -pe micronaut-core.cue -rp https://github.com/micronaut-projects/micronaut-core -b 4.0.x -d 82d115b4901d10226552ac67b0a10978cd5bc603 --skip-deps
+
+where ``micronaut-core.cue`` file can contain:
+
+.. code-block:: javascript
+
+  {
+    target: "micronaut-projects/micronaut-core",
+    predicate: {
+        invocation: {
+            configSource: {
+                uri: =~"^git\\+https://github.com/micronaut-projects/micronaut-core@refs/tags/v[0-9]+.[0-9]+.[0-9]+$"
+                entryPoint: ".github/workflows/release.yml"
+            }
+        }
+    }
+  }
+
+.. note::
+  The provenance expectation is verified via the ``provenance_expectation`` check in Macaron. You can see the result of this check in the HTML or JSON report and see if the provenance found by Macaron meets the expectation CUE file.
+
 ----------------------
 Analyzing with an SBOM
 ----------------------
 
-Macaron can run the analysis against a `CycloneDX <https://cyclonedx.org/>`__ format SBOM, which contains all the necessary information of the target component and its dependencies. This use case is useful when you are running Macaron against a software component that is not available as a public GitHub repository but you still want to analyze the SLSA posture of its dependencies.
+Macaron can run the analysis against an existing SBOM in `CycloneDX <https://cyclonedx.org/>`_ which contains all the necessary information of the dependencies of a target repository. In this case, the dependencies will not be resolved automatically.
 
-CycloneDX provides open-source SBOM generators for different types of project (e.g Maven, Gradle, etc) To know how you could generate an CycloneDX SBOM for your projects, please have a look at their `open-source organization <https://github.com/CycloneDX>`_.
+CycloneDX provides open-source SBOM generators for different types of project (e.g Maven, Gradle, etc). For instructions on generating a CycloneDX SBOM for your project, see `CycloneDX documentation <https://github.com/CycloneDX>`_.
 
 For example, with `micronaut-core <https://github.com/micronaut-projects/micronaut-core>`_ at branch 4.0.x commit ``82d115b4901d10226552ac67b0a10978cd5bc603``, using the `CycloneDX Gradle plugin <https://github.com/CycloneDX/cyclonedx-gradle-plugin>`_ would give us the following `SBOM <./_static/micronaut-projects/micronaut-core/analyze_with_sbom/sbom.json>`_.
 
@@ -101,3 +135,36 @@ With ``rest_of_args`` being the arguments to the ``analyze`` command (e.g. ``-b`
 The ``-lr`` flag configure Macaron to looks into ``path/to/boo/foo`` for local repositories. For more information, please see :ref:`Command Line Usage <cli-usage>`.
 
 .. note:: If ``-lr`` is not provided, Macaron will looks inside ``<working_directory>/output/git_repos/local_repos/`` whenever you provide a local path to ``-rp``.
+
+-------------------------
+Running the policy engine
+-------------------------
+
+Macaron's policy engine accepts policies specified in `Datalog <https://en.wikipedia.org/wiki/Datalog>`_. An example policy
+can verify if a project and all its dependencies pass certain checks. We use `Soufflé <https://souffle-lang.github.io/index.html>`_
+as the Datalog engine in Macaron. Once you run the checks on a target project as described :ref:`here <analyze-action>`,
+the check results will be stored in ``macaron.db`` in the output directory. We can pass the check results to the policy
+engine and provide a Datalog policy file to be enforced by the policy engine.
+
+We use `Micronaut MuShop <https://github.com/oracle-quickstart/oci-micronaut>`_ project as a case study to show how to run the policy engine.
+Micronaut MuShop is a cloud-native microservices example for Oracle Cloud Infrastructure. When we run Macaron on the Micronaut MuShop GitHub
+project, it automatically finds the project’s dependencies and runs checks for the top-level project and dependencies
+independently. For example, the build service check, as defined in SLSA, analyzes the CI configurations to determine if its artifacts are built
+using a build service. Another example is the check that determines whether a SLSA provenance document is available for an artifact. If so, it
+verifies whether the provenance document attests to the produced artifacts. For the Micronaut MuShop project, Macaron identifies 48 dependencies
+that map to 24 unique repositories and generates an HTML report that summarizes the check results.
+
+Now we can run the policy engine over these results and enforce a policy:
+
+.. code-block:: shell
+
+  ./run_macaron.sh verify-policy -o outputs -d outputs/macaron.db --file oci-micronaut.dl
+
+In this example, the Datalog policy file is provided in `oci-micronaut.dl <../_static/examples/oracle-quickstart/oci-micronaut/policies/oci-micronaut.dl>`__.
+This example policy can verify if the Micronaut MuShop project and all its dependencies pass the ``build_service`` check
+and the Micronaut provenance documents meets the expectation provided as a `CUE file <../_static/examples/micronaut-projects/micronaut-core/policies/micronaut-core.cue>`__.
+
+Thanks to Datalog’s expressive language model, it’s easy to add exception rules if certain dependencies do not meet a
+requirement. For example, `the Mysql Connector/J <https://slsa.dev/spec/v0.1/requirements#build-service>`_ dependency in
+the Micronaut MuShop project does not pass the ``build_service`` check, but can be manually investigated and exempted if trusted. Overall, policies expressed in Datalog can be
+enforced by Macaron as part of your CI/CD pipeline to detect regressions or unexpected behavior.