Add wrapper structs for X509/X509_CRL

goatgoose · Sep 28, 2022 · 33a74ef · 33a74ef
1 parent 49c3345
commit 33a74ef
Show file tree

Hide file tree

Showing 16 changed files with 4,329 additions and 1 deletion.
diff --git a/api/s2n.h b/api/s2n.h
@@ -946,6 +946,22 @@ typedef uint8_t (*s2n_verify_host_fn) (const char *host_name, size_t host_name_l
 S2N_API
 extern int s2n_config_set_verify_host_callback(struct s2n_config *config, s2n_verify_host_fn, void *data);
 
+struct s2n_x509_cert;
+
+S2N_API
+extern int s2n_x509_cert_get_issuer_hash(struct s2n_x509_cert *cert, unsigned long *hash);
+
+struct s2n_x509_crl;
+
+S2N_API
+extern int s2n_x509_crl_from_pem(char *pem, struct s2n_x509_crl **crl);
+
+S2N_API
+extern int s2n_x509_crl_free(struct s2n_x509_crl *crl);
+
+S2N_API
+extern int s2n_x509_crl_get_issuer_hash(struct s2n_x509_crl *crl, unsigned long *hash);
+
 /**
  * Toggles whether or not to validate stapled OCSP responses.
  *

diff --git a/stuffer/s2n_stuffer.h b/stuffer/s2n_stuffer.h
@@ -167,6 +167,9 @@ extern int s2n_stuffer_private_key_from_pem(struct s2n_stuffer *pem, struct s2n_
 /* Read a certificate  from a PEM encoded stuffer to an ASN1/DER encoded one */
 extern int s2n_stuffer_certificate_from_pem(struct s2n_stuffer *pem, struct s2n_stuffer *asn1);
 
+/* Read a CRL from a PEM encoded stuffer to an ASN1/DER encoded one */
+extern int s2n_stuffer_crl_from_pem(struct s2n_stuffer *pem, struct s2n_stuffer *asn1);
+
 /* Read DH parameters om a PEM encoded stuffer to a PKCS3 encoded one */
 extern int s2n_stuffer_dhparams_from_pem(struct s2n_stuffer *pem, struct s2n_stuffer *pkcs3);
 

diff --git a/stuffer/s2n_stuffer_pem.c b/stuffer/s2n_stuffer_pem.c
@@ -31,6 +31,7 @@
 #define S2N_PEM_DH_PARAMETERS               "DH PARAMETERS"
 #define S2N_PEM_EC_PARAMETERS               "EC PARAMETERS"
 #define S2N_PEM_CERTIFICATE                 "CERTIFICATE"
+#define S2N_PEM_CRL                         "X509 CRL"
 
 static int s2n_stuffer_pem_read_encapsulation_line(struct s2n_stuffer *pem, const char* encap_marker, const char *keyword) {
 
@@ -165,6 +166,10 @@ int s2n_stuffer_certificate_from_pem(struct s2n_stuffer *pem, struct s2n_stuffer
     return s2n_stuffer_data_from_pem(pem, asn1, S2N_PEM_CERTIFICATE);
 }
 
+int s2n_stuffer_crl_from_pem(struct s2n_stuffer *pem, struct s2n_stuffer *asn1) {
+    return s2n_stuffer_data_from_pem(pem, asn1, S2N_PEM_CRL);
+}
+
 int s2n_stuffer_dhparams_from_pem(struct s2n_stuffer *pem, struct s2n_stuffer *pkcs3)
 {
     return s2n_stuffer_data_from_pem(pem, pkcs3, S2N_PEM_DH_PARAMETERS);

diff --git a/tests/cbmc/proofs/s2n_add_overflow/report/json/viewer-coverage.json b/tests/cbmc/proofs/s2n_add_overflow/report/json/viewer-coverage.json
@@ -0,0 +1,82 @@
+{
+  "viewer-coverage": {
+    "coverage": {
+      "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c": {
+        "s2n_add_overflow_harness": {
+          "24": "hit",
+          "25": "hit",
+          "26": "hit",
+          "28": "hit",
+          "29": "hit",
+          "31": "hit",
+          "33": "hit"
+        }
+      },
+      "tests/cbmc/stubs/s2n_calculate_stacktrace.c": {
+        "s2n_calculate_stacktrace": {
+          "20": "hit"
+        }
+      },
+      "utils/s2n_safety.c": {
+        "s2n_add_overflow": {
+          "199": "both",
+          "200": "hit",
+          "201": "both",
+          "202": "hit",
+          "203": "hit",
+          "204": "hit"
+        }
+      }
+    },
+    "function_coverage": {
+      "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c": {
+        "s2n_add_overflow_harness": {
+          "hit": 7,
+          "percentage": 1.0,
+          "total": 7
+        }
+      },
+      "tests/cbmc/stubs/s2n_calculate_stacktrace.c": {
+        "s2n_calculate_stacktrace": {
+          "hit": 1,
+          "percentage": 1.0,
+          "total": 1
+        }
+      },
+      "utils/s2n_safety.c": {
+        "s2n_add_overflow": {
+          "hit": 6,
+          "percentage": 1.0,
+          "total": 6
+        }
+      }
+    },
+    "line_coverage": {
+      "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c": {
+        "24": "hit",
+        "25": "hit",
+        "26": "hit",
+        "28": "hit",
+        "29": "hit",
+        "31": "hit",
+        "33": "hit"
+      },
+      "tests/cbmc/stubs/s2n_calculate_stacktrace.c": {
+        "20": "hit"
+      },
+      "utils/s2n_safety.c": {
+        "199": "both",
+        "200": "hit",
+        "201": "both",
+        "202": "hit",
+        "203": "hit",
+        "204": "hit"
+      }
+    },
+    "overall_coverage": {
+      "hit": 14,
+      "percentage": 1.0,
+      "total": 14
+    }
+  }
+}
diff --git a/tests/cbmc/proofs/s2n_add_overflow/report/json/viewer-loop.json b/tests/cbmc/proofs/s2n_add_overflow/report/json/viewer-loop.json
@@ -0,0 +1,36 @@
+{
+  "viewer-loop": {
+    "loops": {
+      "s2n_add_overflow.0": {
+        "file": "utils/s2n_safety.c",
+        "function": "s2n_add_overflow",
+        "line": 199
+      },
+      "s2n_add_overflow.1": {
+        "file": "utils/s2n_safety.c",
+        "function": "s2n_add_overflow",
+        "line": 199
+      },
+      "s2n_add_overflow.2": {
+        "file": "utils/s2n_safety.c",
+        "function": "s2n_add_overflow",
+        "line": 199
+      },
+      "s2n_add_overflow.3": {
+        "file": "utils/s2n_safety.c",
+        "function": "s2n_add_overflow",
+        "line": 201
+      },
+      "s2n_add_overflow.4": {
+        "file": "utils/s2n_safety.c",
+        "function": "s2n_add_overflow",
+        "line": 201
+      },
+      "s2n_add_overflow.5": {
+        "file": "utils/s2n_safety.c",
+        "function": "s2n_add_overflow",
+        "line": 201
+      }
+    }
+  }
+}
diff --git a/tests/cbmc/proofs/s2n_add_overflow/report/json/viewer-property.json b/tests/cbmc/proofs/s2n_add_overflow/report/json/viewer-property.json
@@ -0,0 +1,206 @@
+{
+  "viewer-property": {
+    "properties": {
+      "malloc.assertion.1": {
+        "class": "assertion",
+        "description": "max allocation size exceeded",
+        "expression": "malloc_size <= __CPROVER_max_malloc_size",
+        "location": {
+          "file": "<builtin-library-malloc>",
+          "function": "malloc",
+          "line": 28
+        }
+      },
+      "malloc.assertion.2": {
+        "class": "assertion",
+        "description": "max allocation may fail",
+        "expression": "!(1 != 0) || !should_malloc_fail",
+        "location": {
+          "file": "<builtin-library-malloc>",
+          "function": "malloc",
+          "line": 33
+        }
+      },
+      "s2n_add_overflow.overflow.1": {
+        "class": "overflow",
+        "description": "arithmetic overflow on unsigned + in (uint64_t)a + (uint64_t)b",
+        "expression": "!overflow(\"+\", uint64_t, (uint64_t)a, (uint64_t)b)",
+        "location": {
+          "file": "utils/s2n_safety.c",
+          "function": "s2n_add_overflow",
+          "line": 200
+        }
+      },
+      "s2n_add_overflow.overflow.2": {
+        "class": "overflow",
+        "description": "arithmetic overflow on unsigned to unsigned type conversion in (uint32_t)result",
+        "expression": "!(result >= 4294967296ull)",
+        "location": {
+          "file": "utils/s2n_safety.c",
+          "function": "s2n_add_overflow",
+          "line": 202
+        }
+      },
+      "s2n_add_overflow.pointer_dereference.1": {
+        "class": "pointer dereference",
+        "description": "dereference failure: pointer NULL in *out",
+        "expression": "!(POINTER_OBJECT(out) == POINTER_OBJECT(((uint32_t *)NULL)))",
+        "location": {
+          "file": "utils/s2n_safety.c",
+          "function": "s2n_add_overflow",
+          "line": 202
+        }
+      },
+      "s2n_add_overflow.pointer_dereference.2": {
+        "class": "pointer dereference",
+        "description": "dereference failure: pointer invalid in *out",
+        "expression": "!IS_INVALID_POINTER(out)",
+        "location": {
+          "file": "utils/s2n_safety.c",
+          "function": "s2n_add_overflow",
+          "line": 202
+        }
+      },
+      "s2n_add_overflow.pointer_dereference.3": {
+        "class": "pointer dereference",
+        "description": "dereference failure: deallocated dynamic object in *out",
+        "expression": "!(POINTER_OBJECT(out) == POINTER_OBJECT(__CPROVER_deallocated))",
+        "location": {
+          "file": "utils/s2n_safety.c",
+          "function": "s2n_add_overflow",
+          "line": 202
+        }
+      },
+      "s2n_add_overflow.pointer_dereference.4": {
+        "class": "pointer dereference",
+        "description": "dereference failure: dead object in *out",
+        "expression": "!(POINTER_OBJECT(out) == POINTER_OBJECT(__CPROVER_dead_object))",
+        "location": {
+          "file": "utils/s2n_safety.c",
+          "function": "s2n_add_overflow",
+          "line": 202
+        }
+      },
+      "s2n_add_overflow.pointer_dereference.5": {
+        "class": "pointer dereference",
+        "description": "dereference failure: pointer outside object bounds in *out",
+        "expression": "POINTER_OFFSET(out) >= 0l && OBJECT_SIZE(out) >= (unsigned long int)POINTER_OFFSET(out) + 4ul",
+        "location": {
+          "file": "utils/s2n_safety.c",
+          "function": "s2n_add_overflow",
+          "line": 202
+        }
+      },
+      "s2n_add_overflow.pointer_dereference.6": {
+        "class": "pointer dereference",
+        "description": "dereference failure: invalid integer address in *out",
+        "expression": "!(POINTER_OBJECT(((uint32_t *)NULL)) == POINTER_OBJECT(out)) || out == ((uint32_t *)NULL)",
+        "location": {
+          "file": "utils/s2n_safety.c",
+          "function": "s2n_add_overflow",
+          "line": 202
+        }
+      },
+      "s2n_add_overflow_harness.assertion.1": {
+        "class": "assertion",
+        "description": "assertion *out == a + b",
+        "expression": "!((signed long int)(signed long int)!(*out == a + b) != 0l)",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 29
+        }
+      },
+      "s2n_add_overflow_harness.assertion.2": {
+        "class": "assertion",
+        "description": "assertion ( uint64_t )a + ( uint64_t )b > UINT32_MAX || out == NULL",
+        "expression": "!((signed long int)(signed long int)!((uint64_t)a + (uint64_t)b > (unsigned long int)4294967295u || out == ((uint32_t *)NULL)) != 0l)",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 31
+        }
+      },
+      "s2n_add_overflow_harness.overflow.1": {
+        "class": "overflow",
+        "description": "arithmetic overflow on unsigned + in a + b",
+        "expression": "!overflow(\"+\", uint32_t, a, b)",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 29
+        }
+      },
+      "s2n_add_overflow_harness.overflow.2": {
+        "class": "overflow",
+        "description": "arithmetic overflow on unsigned + in (uint64_t)a + (uint64_t)b",
+        "expression": "TRUE ==> !overflow(\"+\", uint64_t, (uint64_t)a, (uint64_t)b)",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 31
+        }
+      },
+      "s2n_add_overflow_harness.pointer_dereference.1": {
+        "class": "pointer dereference",
+        "description": "dereference failure: pointer NULL in *out",
+        "expression": "!(POINTER_OBJECT(out) == POINTER_OBJECT(((uint32_t *)NULL)))",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 29
+        }
+      },
+      "s2n_add_overflow_harness.pointer_dereference.2": {
+        "class": "pointer dereference",
+        "description": "dereference failure: pointer invalid in *out",
+        "expression": "!IS_INVALID_POINTER(out)",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 29
+        }
+      },
+      "s2n_add_overflow_harness.pointer_dereference.3": {
+        "class": "pointer dereference",
+        "description": "dereference failure: deallocated dynamic object in *out",
+        "expression": "!(POINTER_OBJECT(out) == POINTER_OBJECT(__CPROVER_deallocated))",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 29
+        }
+      },
+      "s2n_add_overflow_harness.pointer_dereference.4": {
+        "class": "pointer dereference",
+        "description": "dereference failure: dead object in *out",
+        "expression": "!(POINTER_OBJECT(out) == POINTER_OBJECT(__CPROVER_dead_object))",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 29
+        }
+      },
+      "s2n_add_overflow_harness.pointer_dereference.5": {
+        "class": "pointer dereference",
+        "description": "dereference failure: pointer outside object bounds in *out",
+        "expression": "POINTER_OFFSET(out) >= 0l && OBJECT_SIZE(out) >= (unsigned long int)POINTER_OFFSET(out) + 4ul",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 29
+        }
+      },
+      "s2n_add_overflow_harness.pointer_dereference.6": {
+        "class": "pointer dereference",
+        "description": "dereference failure: invalid integer address in *out",
+        "expression": "!(POINTER_OBJECT(((uint32_t *)NULL)) == POINTER_OBJECT(out)) || out == ((uint32_t *)NULL)",
+        "location": {
+          "file": "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c",
+          "function": "s2n_add_overflow_harness",
+          "line": 29
+        }
+      }
+    }
+  }
+}
diff --git a/tests/cbmc/proofs/s2n_add_overflow/report/json/viewer-reachable.json b/tests/cbmc/proofs/s2n_add_overflow/report/json/viewer-reachable.json
@@ -0,0 +1,15 @@
+{
+  "viewer-reachable": {
+    "reachable": {
+      "tests/cbmc/proofs/s2n_add_overflow/s2n_add_overflow_harness.c": [
+        "s2n_add_overflow_harness"
+      ],
+      "tests/cbmc/stubs/s2n_calculate_stacktrace.c": [
+        "s2n_calculate_stacktrace"
+      ],
+      "utils/s2n_safety.c": [
+        "s2n_add_overflow"
+      ]
+    }
+  }
+}