AWS Proof Build Assistant automatically finds build-related information such as file dependencies, included directories and defines for source files within a c code base. Users can access the AWS Proof Build Assistant through arpa, the command-line interface. This document serves as a reference for using arpa and integrating it into your project.

arpa accumulates build information for a complete c code base inside an internal JSON representation which can be used to generate a Makefile containing all the relevant information for a single given source file. arpa simplifies the task of proof developers by automatically generating a ready-to-use Makefile containing information that developers previously had to find manually. In order to use the generated Makefile, developers must include it in another custom (and possibly trivial) Makefile and run make on it. Its ease of use makes AWS Proof Build Assistant ideal for local proof implementation and building as well as part of CI.

Source code repository

Overview

Consider the following c file, which is a CBMC proof harness (discussed below):

#include "api/s2n.h"
#include "stuffer/s2n_stuffer.h"
#include <assert.h>
#include <cbmc_proof/proof_allocators.h>
#include <cbmc_proof/make_common_datastructures.h>

void s2n_stuffer_alloc_harness() {
    struct s2n_stuffer *stuffer = 
        can_fail_malloc(sizeof(*stuffer));
    struct s2n_blob* in = cbmc_allocate_s2n_blob();

    if (s2n_stuffer_init(stuffer, in) == S2N_SUCCESS){
        assert(s2n_stuffer_is_valid(stuffer));
        assert(s2n_blob_is_valid(in));
    };
}

In order to run the above file as part of a CBMC proof, users must provide to CBMC a collection of build information for the file which consists of:

• Source file dependencies:
  Obtained through static analysis. For this purpose, AWS Proof Build Assistant uses cflow, which generates a function-level call graph.
• Included directories and Defined variables:
  Required for compilation. A compilation command for each source file is generated by setting the -DCMAKE_EXPORT_COMPILE_COMMANDS flag when calling cmake on the code base.

AWS Proof Build Assistant calls the relevant tools, parses the outputs and gathers all the build information within an easy-to-read and easy-to-integrate Makefile that is custom-build for the specific proof harness under test. Users can run the following command:

arpa run                              \
    -file path/to/file_under_test.c   \
    -cc $BLDDIR/compile_commands.json \
    -r  $SRCDIR

Doing so generates the following Makefile, which contains all the relevant build information for the above source file:

DEFINES += -DS2N_HAVE_EXECINFO
DEFINES += -DS2N_NO_PQ_ASM
DEFINES += -D_POSIX_C_SOURCE=200809L

INCLUDES += -I$(SRCDIR)
INCLUDES += -I$(SRCDIR)/api

PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROOF_SOURCES += $(PROOF_SOURCE)/proof_allocators.c

PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

Motivation

Although arpa is capable of generating valuable Makefiles for any source file of a code base, its main use case is in the context of running CBMC proofs. Generally speaking, running a CBMC proof requires users to create a harness (a c source file containing the CBMC call) and a corresponding Makefile. This Makefile should contain all the required build information for the proof harness under test and should include a Makefile.common that contains all the make rules. arpa is useful in this context as it generates a Makefile.arpa that contains all the build information (excluding customizations) that can be included directly in a custom Makefile.

arpa would be ideal for code bases that already contain CBMC proofs. In this context, arpa would be integrated as a submodule inside these code bases and would simplify the development of additional CBMC proofs. Currently, we can envision arpa to be integrated in the following five AWS projects:

• S2n (Integration PR pending)
• AWS C Common
• AWS Encryption sdk
• Amazon FreeRTOS
• AWS Iot device sdk

For Proof Writers

In this section, we provide a step-by-step guide designed to help proof developers integrate AWS Proof Build Assistant into their project and use it for implementation of CBMC Proofs.

Integrating arpa into a project

1. Integrate AWS Proof Build Assistant as a submodule:
   1. Inside your git repository, run:
      

      git submodule add 
          https://github.com/path/to/aws/proof/assistant
      

   2. (Optional) Add the submodule root path to PATH:
      

      export PATH=path/to/submodule/root/dir:$PATH
      

2. Install the required dependencies listed below:
   • Cmake (for tests) - (apt-get install cmake or brew install cmake)
   • GNU cflow - (apt-get install cflow or brew install cflow)
   • Voluptuous - (python3 -m pip install voluptuous)

Using arpa for writing proofs

If your project...

...conforms to the aws-templates-for-cbmc-proofs

1. Further integrate arpa into the project by modifying the included Makefile-project-defines project:
   • Add the path to to the arpa executable :

     ARPA = /path/to/AWS_Proof_Build_Assistant/submodule/arpa
     

   • Add project-specific cmake flags:

     ARPA_CMAKE_FLAGS += --cmake-flag-A
     ARPA_CMAKE_FLAGS += --cmake-flag-B
     ...
     

2. Generate a Makefile.arpa for a given proof harness:
   1. Move to the proof directory which contains a harness source file:

      cd $PROOFDIR
      

   2. Run make arpa (which runs cmake in the background, generates compilation commands, the runs arpa run):

      make arpa
      

   3. This generates a Makefile at $PROOFDIR/Makefile.arpa.

...does not conform to the aws-templates-for-cbmc-proofs

1. Generate the build files (including the compilation commands):
   • Run cmake on the code base using project-specific flags, if necessary:

     cmake [--project-specific-flags]       \
         -DCMAKE_EXPORT_COMPILE_COMMANDS=1  \
         -B $BLDDIR                         \
         -S $SRCDIR
     

   • This generates a JSON file containing compilation commands for each source file at $BLDDIR/compile_commands.json.
   • Currently, arpa can only handle projects that build with cmake.
2. Generate a Makefile.arpa for a given proof harness:
   1. Move to the proof directory which contains a harness source file:

      cd $PROOFDIR
      

   2. Run arpa run:

      arpa run                              \
      -cc $BLDDIR/compile_commands.json \
      -r  $SRCDIR
      

   3. This generates a Makefile at $PROOFDIR/Makefile.arpa.

Running CBMC proofs

1. Create a simple Makefile that calls Makefile.arpa:
   1. In the same directory as the harness, create a simple Makefile that:
      • contains variable name adaptations (if required)
      • contains variable customizations (if required)
      • includes Makefile.arpa
      • includes Makefile.common
   2. Such a Makefile may resemble the following:

      # (Variable name adaptation):
      PROJECT_SPECIFIC_VAR_NAME = $(VAR_NAME_USED_BY_arpa)
      # ex. PROOFSOURCES += $(PROOFSTUB)/sysconf.c 
      
      # (Variable customizations):
      CUSTOM_VAR = CUSTOM_VAL
      # ex. CHECKFLAGS += --bounds-check 
      
      include $PROOFDIR/Makefile.arpa
      include path/to/Makefile.common
      

2. Run CBMC:
   1. While in the directory containing the harness and the Makefile created in step 4, run make to run CBMC.
   2. You may run a command such as:

      make report 
      

Subtool reference

arpa consists of two user-facing commands:

• arpa build:
  generate a JSON file containing the internal representation used by arpa
• arpa run:
  generate a `Makefile` containing build information for a given harness

Regardless of the command, arpa always recreates the internal representation from the command line flags (cmake compilation commands and root directory). As such, the arpa command simply defines how arpa will process the generated internal representation and what artifact arpa will generate.

arpa build

arpa build [-h] -cc FILE [-r DIR] [-jp FILE]

This command generates a JSON file containing the internal representation used by arpa from the compilation commands generated through the cmake call and from the root directory of the project.

-cc FILE, --compile-commands FILE

Path to the compile_commands.json file generated during the cmake call.

-r DIR, --root-dir DIR

Path to the root directory of the project under test. By default, this flag is set to the working directory.

-jp FILE, --json_path FILE

Output path for the generated JSON file. By default, arpa generates an internal_rep.json in the working directory.

arpa run

arpa run [-h] -cc FILE -r DIR [-file FILE] [-sp FILE]
            [-def V] [-inc V] [-ext EXT] 
            [-mrv V] [-mrp DIR] 
            [-msrv V] [-msrp DIR]
            [-mstv V] [-mstp DIR]
            [-mproj V] [-mproo V]

This command generates a Makefile.arpa containing relevant build information for a specified source file given cmake compilation commands and the project root path.

-cc FILE, --compile-commands FILE

Path to the compile_commands.json file generated during the cmake call.

-r DIR, --root-dir DIR

Path to the root directory of the project under test.

-file FILE, --file-under-test FILE

Path to the harness source file under test for which a Makefile.arpa will be generated. By default, arpa will search the working directory for a file that ends with "_harness.c". If the number of such files in the working directory is not exactly 1, arpa will throw an error.

-sp FILE, --save_path FILE

Output path for the generated Makefile. By default, arpa generates a Makefile.arpa in the working directory.