[coreSNTP] CBMC Proof for Sntp_SerializeRequest Function (#10)

* Set up litani infra for coreSNTP

* Add content to README.md (#9)

* Add Sntp_Init API for higher-layer of coreSNTP (#8)

Start development of the higher-layer part of the coreSNTP library that represents a "managed client" functionality by adding the Sntp_Init API to initialize an Sntp context.

* Revert "Set up litani infra for coreSNTP"

This reverts commit 6f2017e.

* Sntp_SerializeRequest CBMC Proof

* Updating run-cbmc-proofs.py file permissions

Co-authored-by: Archit Aggarwal <[email protected]>

source/core_sntp_serializer.c

@@ -165,9 +165,9 @@ static void fillWordMemoryInNetworkOrder( uint32_t * pWordMemory,
     assert( pWordMemory != NULL );
 
     *( ( uint8_t * ) pWordMemory ) = ( uint8_t ) ( data >> 24 );
-    *( ( uint8_t * ) pWordMemory + 1 ) = ( uint8_t ) ( data >> 16 );
-    *( ( uint8_t * ) pWordMemory + 2 ) = ( uint8_t ) ( data >> 8 );
-    *( ( uint8_t * ) pWordMemory + 3 ) = ( uint8_t ) data;
+    *( ( uint8_t * ) pWordMemory + 1 ) = ( uint8_t ) ( ( data >> 16 ) & 0x000000FF );
+    *( ( uint8_t * ) pWordMemory + 2 ) = ( uint8_t ) ( ( data >> 8 ) & 0x000000FF );
+    *( ( uint8_t * ) pWordMemory + 3 ) = ( uint8_t ) ( ( data ) & 0x000000FF );
 }
 
 /**

source/include/core_sntp_serializer.h

@@ -33,6 +33,7 @@
 
 /* Standard include. */
 #include <stdint.h>
+#include <stddef.h>
 
 /**
  * @brief The base packet size of request and response of the (S)NTP protocol.

test/cbmc/proofs/Sntp_SerializeRequest/Makefile

@@ -0,0 +1,20 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = Sntp_SerializeRequest_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = Sntp_SerializeRequest
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_serializer.c
+
+include ../Makefile.common

test/cbmc/proofs/Sntp_SerializeRequest/README.md

@@ -0,0 +1,23 @@
+Sntp_SerializeRequest proof
+==============
+
+This directory contains a memory safety proof for Sntp_SerializeRequest.
+
+The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of:
+ * Sntp_SerializeRequest()
+
+To run the proof.
+-------------
+
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path.
+* Run `make`.
+* Open html/index.html in a web browser.
+
+To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles.
+-------------
+
+* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
+* Use Makefile.arpa as the starting point for your proof Makefile by:
+  1. Modifying Makefile.arpa (if required).
+  2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).

test/cbmc/proofs/Sntp_SerializeRequest/Sntp_SerializeRequest_harness.c

@@ -0,0 +1,48 @@
+/*
+ * coreSNTP v1.0.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/**
+ * @file Sntp_SerializeRequest_harness.c
+ * @brief Implements the proof harness for Sntp_SerializeRequest function.
+ */
+
+#include <stdint.h>
+#include "core_sntp_serializer.h"
+
+void harness()
+{
+    SntpTimestamp_t * pRequestTime;
+    uint32_t randomNumber;
+    void * pBuffer;
+    size_t bufferSize;
+    SntpStatus_t sntpStatus;
+
+    pRequestTime = malloc( sizeof( SntpTimestamp_t ) );
+
+    __CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE );
+
+    pBuffer = malloc( bufferSize );
+
+    sntpStatus = Sntp_SerializeRequest( pRequestTime, randomNumber, pBuffer, bufferSize );
+
+    __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpErrorBufferTooSmall || sntpStatus == SntpSuccess ), "The return value is a valid SNTP Status" );
+}

test/cbmc/proofs/Sntp_SerializeRequest/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

test/cbmc/proofs/Sntp_SerializeRequest/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "Sntp_SerializeRequest",
+  "proof-root": "test/cbmc/proofs"
+}