[CoreSNTP]Sntp deserialize response and Sntp_SendTimeRequest cbmc proofs

.github/workflows/ci.yml

@@ -69,7 +69,7 @@ jobs:
           -G "Unix Makefiles" \
           -DCMAKE_BUILD_TYPE=Debug \
           -DBUILD_CLONE_SUBMODULES=ON \
-          -DCMAKE_C_FLAGS='--coverage -Wall -Wextra -Werror -DNDEBUG -Wno-error=pedantic -Wno-variadic-macros -DLOGGING_LEVEL_DEBUG=1'
+          -DCMAKE_C_FLAGS='--coverage -Wall -Wextra -Werror -DNDEBUG -Wno-error=pedantic -Wno-variadic-macros -Wno-error=unknown-pragmas -DLOGGING_LEVEL_DEBUG=1'
           make -C build/ all
       - name: Test
         run: |

lexicon.txt

@@ -12,12 +12,15 @@ beforelooptime
 blocktimems
 br
 buffersize
+bytesorerror
 bytesremaining
 bytessent
 bytestorecv
 bytestorecv
 bytestosend
 bytestosend
+cbmc
+clienttime
 clienttxtime
 clockfreqtolerance
 clockoffsetsec
@@ -45,6 +48,7 @@ expectedinterval
 expectedtxtime
 faqs
 feb
+firstorderdiff
 fracs
 fracsinnetorder
 fracsinnetorder
@@ -62,6 +66,7 @@ ifndef
 inc
 ingroup
 inlooptime
+int
 iot
 ip
 iso
@@ -73,6 +78,8 @@ leapsecondinfo
 leapversionmode
 lsb
 misra
+networkinterfacereceivestub
+networkinterfacesendstub
 nist
 noleapsecond
 noninfringement
@@ -156,7 +163,10 @@ serveraddr
 servernamelen
 serverport
 serverresponsetimeoutms
+servertime
 setsystemtimefunc
+signedfirstorderdiffrecv
+signedfirstorderdiffsend
 sizeof
 sntp
 sntpbuffertoosmall
@@ -186,6 +196,7 @@ startingpos
 struct
 sublicense
 testbuffer
+testclockoffsetcalculation
 timebeforeloop
 timeserver
 transmittime

source/core_sntp_serializer.c

@@ -191,6 +191,87 @@ static uint32_t readWordFromNetworkByteOrderMemory( const uint32_t * ptr )
                           ( ( uint32_t ) *( pMemStartByte + 3 ) ) );
 }
 
+/**
+ * @brief Utility to determine whether the passed first order difference value
+ * between server and client timestamps represents that the server and client
+ * are within 34 years of each other to be able to calculate the clock-offset
+ * value according to the NTPv4 specification's on-wire protocol.
+ *
+ * @param[in] firstOrderDiff A first-order difference value between the client
+ * and server.
+ *
+ * @note As the SNTP timestamp value wraps around after ~136 years (exactly at
+ * 7 Feb 2036 6h 28m 16s), the utility logic checks the first order difference
+ * in both polarities (i.e. as (Server - Client) and (Client - Server) time values )
+ * to support the edge case when the two timestamps are in different SNTP eras (for
+ * example, server time is in 2037 and client time is in 2035 ).
+ */
+static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
+{
+    /* Note: The (UINT32_MAX  - firstOrderDiff + 1U) expression represents
+     * 2's complement or negation of value.
+     * This is done to be compliant with both CBMC and MISRA Rule 10.1.
+     * CBMC flags overflow for (unsigned int = 0U - positive value) whereas
+     * MISRA rule forbids use of unary minus operator on unsigned integers. */
+    return( ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ||
+            ( ( ( UINT32_MAX - firstOrderDiff + 1U ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) );
+}
+
+/**
+ * @brief Utility to perform a safe subtraction operation of unsigned integers and
+ * return the value as a signed integer. This function returns the effective subtraction
+ * value as ( @p minuend - @p subtrahend ).
+ *
+ * @note This utility provides safe subtraction result that involve the following 2 operations::
+ *  * Safe subtraction between unsigned integers
+ *                    AND
+ *  * Safe conversion of unsigned integer to signed integer
+ *
+ * @param[in] minuend The value to subtract from.
+ * @param[in] subtrahend The amount of value to subtract from @p minuend.
+ *
+ * @return The calculated signed subtraction value between the unsigned integers.
+ */
+static int32_t safeSignedSubtraction( uint32_t minuend,
+                                      uint32_t subtrahend )
+{
+    int32_t calculatedValue = 0;
+
+    /* The correct polarity of subtraction is "minuend - subtrahend"
+     * but to avoid overflow in subtraction of unsigned integers, we perform
+     * subtraction in the polarity that generates a positive value. */
+    bool polarity = ( minuend > subtrahend ) ? true : false;
+    uint32_t positiveDiff = ( polarity == true ) ? minuend - subtrahend :
+                            subtrahend - minuend;
+
+    /* Check whether the difference value cannot be represented as a signed
+     * integer without some modification.*/
+    if( positiveDiff > INT32_MAX )
+    {
+        /* Perform 2's complement inversion of the value to convert it to a value less
+         * than INT32_MAX.
+         * Note: The following expression is used for 2's complement operation to be
+         * compliant with both CBMC and MISRA Rule 10.1.
+         * CBMC flags overflow for (unsigned int = 0U - positive value) whereas
+         * MISRA rule forbids use of unary minus operator on unsigned integers.  */
+        positiveDiff = UINT32_MAX - positiveDiff + 1U;
+
+        /* Reverse the state of the polarity as we performed the 2's complement. */
+        polarity = !polarity;
+    }
+
+    /* Now safely, store the unsigned value as a signed integer. */
+    calculatedValue = positiveDiff;
+
+    /* Restore the difference value to represent subtraction in the polarity of "minuend  - subtrahend". */
+    if( polarity == false )
+    {
+        calculatedValue = 0 - calculatedValue;
+    }
+
+    return calculatedValue;
+}
+
 /**
  * @brief Utility to calculate clock offset of system relative to the
  * server using the on-wire protocol specified in the NTPv4 specification.
@@ -259,50 +340,59 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
     SntpStatus_t status = SntpSuccess;
 
     /* Variable for storing the first-order difference between timestamps. */
-    uint32_t firstOrderDiff = 0;
+    uint32_t firstOrderDiffSend = 0;
+    uint32_t firstOrderDiffRecv = 0;
 
     assert( pClientTxTime != NULL );
     assert( pServerRxTime != NULL );
     assert( pServerTxTime != NULL );
     assert( pClientRxTime != NULL );
     assert( pClockOffset != NULL );
 
-    /* Calculate a sample first order difference value between the
-     * server and system timestamps. */
-    firstOrderDiff = pClientRxTime->seconds - pServerTxTime->seconds;
+    /* Calculate first order difference values between the server and system timestamps
+     * to determine whether they are within 34 years of each other. */
+
+    /* To avoid overflow issue, we will store only the positive first order differences of
+     * the timestamps in the unsigned integer now, and later store the values with correct
+     * subtraction polarity (i.e. "Server Time - Client Time") later. */
+    firstOrderDiffSend = ( pServerRxTime->seconds >= pClientTxTime->seconds ) ?
+                         ( pServerRxTime->seconds - pClientTxTime->seconds ) :
+                         ( pClientTxTime->seconds - pServerRxTime->seconds );
+    firstOrderDiffRecv = ( pServerTxTime->seconds >= pClientRxTime->seconds ) ?
+                         ( pServerTxTime->seconds - pClientRxTime->seconds ) :
+                         ( pClientRxTime->seconds - pServerTxTime->seconds );
 
-    /* Determine from the first order difference if the system time is within
+    /* Determine from the first order differences if the system time is within
      * 34 years of server time to be able to calculate clock offset.
-     *
-     * Note: As the SNTP timestamp value wraps around after ~136 years (exactly at
-     * 7 Feb 2036 6h 28m 16s), the conditional logic checks first order difference
-     * in both polarities (i.e. as (Server - Client) and (Client - Server) time values )
-     * to support the edge case when the two timestamps are in different SNTP eras (for
-     * example, server time is in 2037 and client time is in 2035 ).
      */
-    if( ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK )
-          == 0U ) ||
-        ( ( ( 0U - firstOrderDiff ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK )
-          == 0U ) )
+    if( isEligibleForClockOffsetCalculation( firstOrderDiffSend ) &&
+        isEligibleForClockOffsetCalculation( firstOrderDiffRecv ) )
     {
-        /* Calculate the clock-offset as system time is within 34 years window
-         * of server time. */
-        uint32_t firstOrderDiffSend;
-        uint32_t firstOrderDiffRecv;
-        uint32_t sumOfFirstOrderDiffs;
-
-        /* Perform ( T2 - T1 ) offset calculation of SNTP Request packet path. */
-        firstOrderDiffSend = pServerRxTime->seconds - pClientTxTime->seconds;
-
-        /* Perform ( T3 - T4 ) offset calculation of SNTP Response packet path. */
-        firstOrderDiffRecv = 0U - firstOrderDiff;
-
-        /* Perform second order calculation of using average of the above offsets. */
-        sumOfFirstOrderDiffs = firstOrderDiffSend + firstOrderDiffRecv;
+        /* Now that we have validated that system and server times are within 34 years
+         * of each other, we will prepare for the clock-offset calculation. To calculate
+         * clock-offset, the first order difference values need to be stored as signed integers
+         * in the correct polarity of differences according to the formula. */
+        int32_t signedFirstOrderDiffSend = 0;
+        int32_t signedFirstOrderDiffRecv = 0;
+
+        /* Calculate the first order differences in the correct subtraction direction as
+         * "Server Time - Client Time" on both SNTP request and SNTP response network paths. */
+        signedFirstOrderDiffSend = safeSignedSubtraction( pServerRxTime->seconds, pClientTxTime->seconds );
+        signedFirstOrderDiffRecv = safeSignedSubtraction( pServerTxTime->seconds, pClientRxTime->seconds );
+
+        /* We are now sure that each of the first order differences represents the values in
+         * the correct direction of polarities, i.e.
+         * signedFirstOrderDiffSend represents (T2 - T1)
+         *                AND
+         * signedFirstOrderDiffRecv represents (T3 - T4)
+         *
+         * We are now safe to complete the calculation of the clock-offset as the average
+         * of the signed first order difference values.
+         */
 
         /* Use division instead of a bit shift to guarantee sign extension
          * regardless of compiler implementation. */
-        *pClockOffset = ( ( int32_t ) sumOfFirstOrderDiffs / 2 );
+        *pClockOffset = ( ( signedFirstOrderDiffSend + signedFirstOrderDiffRecv ) / 2 );
     }
     else
     {

test/cbmc/include/core_sntp_cbmc_state.h

@@ -0,0 +1,53 @@
+/*
+ * 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 core_sntp_cbmc_state.h
+ * @brief Allocation and assumption utilities for the SNTP library CBMC proofs.
+ */
+#ifndef CORE_SNTP_CBMC_STATE_H_
+#define CORE_SNTP_CBMC_STATE_H_
+
+#include "core_sntp_client.h"
+
+/* Application defined Network context. */
+struct NetworkContext
+{
+    void * networkContext;
+};
+
+/* Application defined authentication context. */
+struct SntpAuthContext
+{
+    void * authContext;
+};
+
+/**
+ * @brief Allocate a #SntpContext_t object.
+ *
+ * @param[in] pContext #SntpContext_t object information.
+ *
+ * @return NULL or allocated #SntpContext_t memory.
+ */
+SntpContext_t * allocateCoreSntpContext( SntpContext_t * pContext );
+
+#endif /* ifndef CORE_SNTP_CBMC_STATE_H_ */