From 439d7e1a44303b2d524301cdd8d4e5bb2e05bda7 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 01:08:23 +0000
Subject: [PATCH 01/17] Refactor calculateClockOffset to avoid overflow issues

---
 source/core_sntp_serializer.c               | 131 ++++++++++++++++----
 test/unit-test/core_sntp_serializer_utest.c |  18 ++-
 2 files changed, 121 insertions(+), 28 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index cb92c97..a268e56 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -121,6 +121,18 @@
  */
 #define CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK    ( 0xC0000000U )
 
+/**
+ * @brief The bit mask for the most-significant bit in an unsigned 32 bit integer.
+ * This value is used in the intermediate conversion of unsigned integer to signed
+ * integer for the first order difference values during clock-offset calculation.
+ *
+ * @note The conversion from unsigned to signed integer of first order difference
+ * values uses this macro to check whether assignment of the unsigned value to signed
+ * integer will overflow, and accordingly, change the unsigned value to safely perform
+ * the conversion.
+ */
+#define UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK                ( 0x80000000U )
+
 /**
  * @brief Structure representing an SNTP packet header.
  * For more information on SNTP packet format, refer to
@@ -191,6 +203,25 @@ 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 ).
+ */
+#define IS_ELIGIBILE_FOR_CLOCK_OFFSET( firstOrderDiff )                                  \
+    ( ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) || \
+      ( ( ( 0U - firstOrderDiff ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) )
+
 /**
  * @brief Utility to calculate clock offset of system relative to the
  * server using the on-wire protocol specified in the NTPv4 specification.
@@ -259,7 +290,9 @@ 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;
+    bool sendPolarity, recvPolarity;
 
     assert( pClientTxTime != NULL );
     assert( pServerRxTime != NULL );
@@ -267,42 +300,86 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
     assert( pClientRxTime != NULL );
     assert( pClockOffset != NULL );
 
-    /* Calculate a sample first order difference value between the
-     * server and system timestamps. */
-    firstOrderDiff = pClientRxTime->seconds - pServerTxTime->seconds;
+    /* On-wire protocol formula's polarity for first order difference in the send network
+     * path is T2 (Server Rx) - T1 (Client TX) .*/
+    recvPolarity = ( pServerTxTime->seconds >= pClientRxTime->seconds ) ? true : false;
+
+    /* On-wire protocol formula's polarity for first order difference in the receive network
+     * path is T3 (Server TX) - T4 (Client RX) .*/
+    sendPolarity = ( pServerRxTime->seconds >= pClientTxTime->seconds ) ? true : false;
 
-    /* Determine from the first order difference if the system time is within
+    /* 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 difference
+     * values in the unsigned integer now, and later store the values with correct polarity
+     * (according to the formula) later. */
+    firstOrderDiffSend = sendPolarity ? ( pServerRxTime->seconds - pClientTxTime->seconds ) :
+                         ( pClientTxTime->seconds - pServerRxTime->seconds );
+    firstOrderDiffRecv = recvPolarity ? ( pServerTxTime->seconds - pClientRxTime->seconds ) :
+                         ( pClientRxTime->seconds - pServerTxTime->seconds );
+
+    /* 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( IS_ELIGIBILE_FOR_CLOCK_OFFSET( firstOrderDiffSend ) &&
+        IS_ELIGIBILE_FOR_CLOCK_OFFSET( 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;
+        /* 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;
+
+        /* To avoid overflow issues in assigning the unsigned values of first order differences
+         * to signed integers, we will inverse the values if they represent a large value that cannot be
+         * represented in a signed integer. */
+        if( ( firstOrderDiffSend & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK ) 
+        == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
+
+        {
+            firstOrderDiffSend = 0U - firstOrderDiffSend;
+            sendPolarity = !sendPolarity;
+        }
 
-        /* Perform ( T2 - T1 ) offset calculation of SNTP Request packet path. */
-        firstOrderDiffSend = pServerRxTime->seconds - pClientTxTime->seconds;
+        if( ( firstOrderDiffRecv & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK ) 
+        == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
 
-        /* Perform ( T3 - T4 ) offset calculation of SNTP Response packet path. */
-        firstOrderDiffRecv = 0U - firstOrderDiff;
+        {
+            firstOrderDiffRecv = 0U - firstOrderDiffRecv;
+            recvPolarity = !recvPolarity;
+        }
 
-        /* Perform second order calculation of using average of the above offsets. */
-        sumOfFirstOrderDiffs = firstOrderDiffSend + firstOrderDiffRecv;
+        /* Now we can safely store the first order differences as signed integer values. */
+        signedFirstOrderDiffSend = firstOrderDiffSend;
+        signedFirstOrderDiffRecv = firstOrderDiffRecv;
+
+        /* To calculate the clock-offset value, we will correct the signed first order difference
+        * values to match the subtraction polarity direction of "Server Time" - "Client Time". */
+        if( sendPolarity == false )
+        {
+            signedFirstOrderDiffSend = 0 - signedFirstOrderDiffSend;
+        }
+
+        if( recvPolarity == false )
+        {
+            signedFirstOrderDiffRecv = 0 - signedFirstOrderDiffRecv;
+        }
+
+        /* 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
     {
diff --git a/test/unit-test/core_sntp_serializer_utest.c b/test/unit-test/core_sntp_serializer_utest.c
index f7ecca0..5e30f99 100644
--- a/test/unit-test/core_sntp_serializer_utest.c
+++ b/test/unit-test/core_sntp_serializer_utest.c
@@ -441,7 +441,7 @@ void test_DeserializeResponse_KoD_packets( void )
  * SNTP server response, and determine that the clock offset cannot be calculated
  * when the client clock is beyond 34 years from server.
  */
-void test_DeserializeResponse_AcceptedResponse_Overflow_Case( void )
+void test_DeserializeResponse_AcceptedResponse_Overflow_Cases( void )
 {
     SntpTimestamp_t clientTime = TEST_TIMESTAMP;
 
@@ -465,6 +465,22 @@ void test_DeserializeResponse_AcceptedResponse_Overflow_Case( void )
                                 &serverTime, &clientTime,
                                 SntpClockOffsetOverflow,
                                 SNTP_CLOCK_OFFSET_OVERFLOW );
+
+    /* Now test the contrived case when only the send network path
+     * represents timestamps that overflow but the receive network path
+     * has timestamps that do not overflow. */
+    testClockOffsetCalculation( &clientTime, &serverTime, /* Send Path times are 40 years apart */
+                                &serverTime, &serverTime, /* Receive path times are the same. */
+                                SntpClockOffsetOverflow,
+                                SNTP_CLOCK_OFFSET_OVERFLOW );
+
+    /* Now test the contrived case when only the receive network path
+     * represents timestamps that overflow but the send network path
+     * has timestamps that do not overflow. */
+    testClockOffsetCalculation( &clientTime, &clientTime, /* Send Path times are the same, i.e. don't overflow */
+                                &serverTime, &clientTime, /* Receive path times are 40 years apart. */
+                                SntpClockOffsetOverflow,
+                                SNTP_CLOCK_OFFSET_OVERFLOW );
 }
 
 /**

From 078efd3fe19e3c36334c378395187d524850f6c6 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 01:19:59 +0000
Subject: [PATCH 02/17] Address CI check failures

---
 lexicon.txt                   | 5 +++++
 source/core_sntp_serializer.c | 8 ++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/lexicon.txt b/lexicon.txt
index 62338fa..adad069 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -16,6 +16,7 @@ bytestorecv
 bytestorecv
 bytestosend
 bytestosend
+clienttime
 clienttxtime
 clockfreqtolerance
 clockoffsetsec
@@ -41,6 +42,7 @@ expectedinterval
 expectedtxtime
 faqs
 feb
+firstorderdiff 
 fracs
 fracsinnetorder
 fracsinnetorder
@@ -149,7 +151,9 @@ serializerequest
 serveraddr
 servernamelen
 serverport
+servertime
 setsystemtimefunc
+signedfirstorderdiffrecv 
 sizeof
 sntp
 sntpbuffertoosmall
@@ -176,6 +180,7 @@ startingpos
 struct
 sublicense
 testbuffer
+testclockoffsetcalculation
 timebeforeloop
 timeserver
 transmittime
diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index a268e56..5086b3a 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -335,16 +335,16 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
         /* To avoid overflow issues in assigning the unsigned values of first order differences
          * to signed integers, we will inverse the values if they represent a large value that cannot be
          * represented in a signed integer. */
-        if( ( firstOrderDiffSend & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK ) 
-        == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
+        if( ( firstOrderDiffSend & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
+            == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
 
         {
             firstOrderDiffSend = 0U - firstOrderDiffSend;
             sendPolarity = !sendPolarity;
         }
 
-        if( ( firstOrderDiffRecv & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK ) 
-        == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
+        if( ( firstOrderDiffRecv & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
+            == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
 
         {
             firstOrderDiffRecv = 0U - firstOrderDiffRecv;

From f4723d9108a8dc590178eb20f32ac2fca2a2e99a Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 01:22:34 +0000
Subject: [PATCH 03/17] Address MISRA Rule 20.7 and 10.3 violations

---
 source/core_sntp_serializer.c | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index 5086b3a..57b0db3 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -218,9 +218,11 @@ static uint32_t readWordFromNetworkByteOrderMemory( const uint32_t * ptr )
  * 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 ).
  */
-#define IS_ELIGIBILE_FOR_CLOCK_OFFSET( firstOrderDiff )                                  \
-    ( ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) || \
-      ( ( ( 0U - firstOrderDiff ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) )
+static bool isEligibileForClockOffsetCalculation( uint32_t firstOrderDiff )
+{
+    return( ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ||
+            ( ( ( 0U - firstOrderDiff ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) );
+}
 
 /**
  * @brief Utility to calculate clock offset of system relative to the
@@ -322,8 +324,8 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
     /* Determine from the first order differences if the system time is within
      * 34 years of server time to be able to calculate clock offset.
      */
-    if( IS_ELIGIBILE_FOR_CLOCK_OFFSET( firstOrderDiffSend ) &&
-        IS_ELIGIBILE_FOR_CLOCK_OFFSET( firstOrderDiffRecv ) )
+    if( isEligibileForClockOffsetCalculation( firstOrderDiffSend ) &&
+        isEligibileForClockOffsetCalculation( 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
@@ -352,8 +354,8 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
         }
 
         /* Now we can safely store the first order differences as signed integer values. */
-        signedFirstOrderDiffSend = firstOrderDiffSend;
-        signedFirstOrderDiffRecv = firstOrderDiffRecv;
+        signedFirstOrderDiffSend = ( int32_t ) firstOrderDiffSend;
+        signedFirstOrderDiffRecv = ( int32_t ) firstOrderDiffRecv;
 
         /* To calculate the clock-offset value, we will correct the signed first order difference
         * values to match the subtraction polarity direction of "Server Time" - "Client Time". */

From 773d71f596b1b30570ad3dcd27522fd00f653a54 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 01:31:35 +0000
Subject: [PATCH 04/17] Fix spellcheck and formattion failures

---
 lexicon.txt | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/lexicon.txt b/lexicon.txt
index adad069..e199e93 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -42,7 +42,7 @@ expectedinterval
 expectedtxtime
 faqs
 feb
-firstorderdiff 
+firstorderdiff
 fracs
 fracsinnetorder
 fracsinnetorder
@@ -153,7 +153,8 @@ servernamelen
 serverport
 servertime
 setsystemtimefunc
-signedfirstorderdiffrecv 
+signedfirstorderdiffrecv
+signedfirstorderdiffsend
 sizeof
 sntp
 sntpbuffertoosmall

From d35dad72e6e8717f3dbc9272457c14863cba66bc Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 02:09:42 +0000
Subject: [PATCH 05/17] Fix typo in internal function name

---
 source/core_sntp_serializer.c | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index 57b0db3..abdfe8a 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -218,7 +218,7 @@ static uint32_t readWordFromNetworkByteOrderMemory( const uint32_t * ptr )
  * 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 isEligibileForClockOffsetCalculation( uint32_t firstOrderDiff )
+static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
 {
     return( ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ||
             ( ( ( 0U - firstOrderDiff ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) );
@@ -324,8 +324,8 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
     /* Determine from the first order differences if the system time is within
      * 34 years of server time to be able to calculate clock offset.
      */
-    if( isEligibileForClockOffsetCalculation( firstOrderDiffSend ) &&
-        isEligibileForClockOffsetCalculation( firstOrderDiffRecv ) )
+    if( isEligibleForClockOffsetCalculation( firstOrderDiffSend ) &&
+        isEligibleForClockOffsetCalculation( 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

From fcee1365632eb4067d821b08980211552eafe05d Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 02:20:18 +0000
Subject: [PATCH 06/17] Replace (0U - unsigned integer) expression with 2s
 complement operation to CBMC compliant

---
 source/core_sntp_serializer.c | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index abdfe8a..56582cf 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -220,8 +220,12 @@ static uint32_t readWordFromNetworkByteOrderMemory( const uint32_t * ptr )
  */
 static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
 {
+    /* Note: The (1U + ~firstOrderDiff) 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 ) ||
-            ( ( ( 0U - firstOrderDiff ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) );
+            ( ( ( 1U + ~firstOrderDiff ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) );
 }
 
 /**
@@ -341,7 +345,11 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
             == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
 
         {
-            firstOrderDiffSend = 0U - firstOrderDiffSend;
+            /* Negate the unsigned integer by performing 2's complement operation.
+             * Note: 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. */
+            firstOrderDiffSend = 1U + ~firstOrderDiffSend;
             sendPolarity = !sendPolarity;
         }
 
@@ -349,7 +357,11 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
             == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
 
         {
-            firstOrderDiffRecv = 0U - firstOrderDiffRecv;
+            /* Negate the unsigned integer by performing 2's complement operation.
+             * Note: 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. */
+            firstOrderDiffRecv = 1U + ~firstOrderDiffRecv;
             recvPolarity = !recvPolarity;
         }
 

From 3240432deddac0fbc3aa7f53bf05609a6db25dab Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 02:34:47 +0000
Subject: [PATCH 07/17] More minor hygiene

---
 source/core_sntp_serializer.c | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index 56582cf..f241f54 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -220,12 +220,12 @@ static uint32_t readWordFromNetworkByteOrderMemory( const uint32_t * ptr )
  */
 static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
 {
-    /* Note: The (1U + ~firstOrderDiff) expression represents 2's complement or negation of value.
+    /* Note: The (~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 ) ||
-            ( ( ( 1U + ~firstOrderDiff ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) );
+            ( ( ( ~firstOrderDiff + 1U ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) );
 }
 
 /**
@@ -307,12 +307,12 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
     assert( pClockOffset != NULL );
 
     /* On-wire protocol formula's polarity for first order difference in the send network
-     * path is T2 (Server Rx) - T1 (Client TX) .*/
-    recvPolarity = ( pServerTxTime->seconds >= pClientRxTime->seconds ) ? true : false;
+     * path is T2 (Server Rx) - T1 (Client Tx) .*/
+    sendPolarity = ( pServerRxTime->seconds >= pClientTxTime->seconds ) ? true : false;
 
     /* On-wire protocol formula's polarity for first order difference in the receive network
-     * path is T3 (Server TX) - T4 (Client RX) .*/
-    sendPolarity = ( pServerRxTime->seconds >= pClientTxTime->seconds ) ? true : false;
+     * path is T3 (Server Tx) - T4 (Client Rx) .*/
+    recvPolarity = ( pServerTxTime->seconds >= pClientRxTime->seconds ) ? true : false;
 
     /* Calculate first order difference values between the server and system timestamps
      * to determine whether they are within 34 years of each other. */
@@ -349,7 +349,7 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
              * Note: 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. */
-            firstOrderDiffSend = 1U + ~firstOrderDiffSend;
+            firstOrderDiffSend = ~firstOrderDiffSend + 1U;
             sendPolarity = !sendPolarity;
         }
 
@@ -361,7 +361,7 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
              * Note: 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. */
-            firstOrderDiffRecv = 1U + ~firstOrderDiffRecv;
+            firstOrderDiffRecv = ~firstOrderDiffRecv + 1U;
             recvPolarity = !recvPolarity;
         }
 

From a069f2594351c5cefe757785af96ccf27fb4c436 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 02:37:08 +0000
Subject: [PATCH 08/17] Fix spellings

---
 lexicon.txt | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/lexicon.txt b/lexicon.txt
index e199e93..00a956d 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -16,6 +16,7 @@ bytestorecv
 bytestorecv
 bytestosend
 bytestosend
+cbmc
 clienttime
 clienttxtime
 clockfreqtolerance
@@ -60,6 +61,7 @@ ifndef
 inc
 ingroup
 inlooptime
+int
 iot
 ip
 iso

From c2fc42edd8a65ba2e90e2fb3976d2fda2c89be83 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 22:07:56 +0000
Subject: [PATCH 09/17] Remove  some complexity of refactoring in the code
 section after eligibility check

---
 source/core_sntp_serializer.c | 34 ++++------------------------------
 1 file changed, 4 insertions(+), 30 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index f241f54..32c6045 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -220,12 +220,13 @@ static uint32_t readWordFromNetworkByteOrderMemory( const uint32_t * ptr )
  */
 static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
 {
-    /* Note: The (~firstOrderDiff + 1U) expression represents 2's complement or negation of value.
+    /* 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 ) ||
-            ( ( ( ~firstOrderDiff + 1U ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) );
+            ( ( ( UINT32_MAX - firstOrderDiff + 1U ) & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) );
 }
 
 /**
@@ -338,33 +339,6 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
         int32_t signedFirstOrderDiffSend = 0;
         int32_t signedFirstOrderDiffRecv = 0;
 
-        /* To avoid overflow issues in assigning the unsigned values of first order differences
-         * to signed integers, we will inverse the values if they represent a large value that cannot be
-         * represented in a signed integer. */
-        if( ( firstOrderDiffSend & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
-            == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
-
-        {
-            /* Negate the unsigned integer by performing 2's complement operation.
-             * Note: 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. */
-            firstOrderDiffSend = ~firstOrderDiffSend + 1U;
-            sendPolarity = !sendPolarity;
-        }
-
-        if( ( firstOrderDiffRecv & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
-            == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
-
-        {
-            /* Negate the unsigned integer by performing 2's complement operation.
-             * Note: 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. */
-            firstOrderDiffRecv = ~firstOrderDiffRecv + 1U;
-            recvPolarity = !recvPolarity;
-        }
-
         /* Now we can safely store the first order differences as signed integer values. */
         signedFirstOrderDiffSend = ( int32_t ) firstOrderDiffSend;
         signedFirstOrderDiffRecv = ( int32_t ) firstOrderDiffRecv;
@@ -385,7 +359,7 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
          * the correct direction of polarities, i.e.
          * signedFirstOrderDiffSend represents (T2 - T1)
          *                AND
-         *  signedFirstOrderDiffRecv represents (T3 - T4)
+         * 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.

From 52c0399ad1f310ab3716dbf1699e0e6ae32ff491 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 23:29:34 +0000
Subject: [PATCH 10/17] Encapsulate operations for signed var = subtraction of
 unsigned integers in internal function

---
 source/core_sntp_serializer.c | 74 ++++++++++++++++++++++++++++-------
 1 file changed, 59 insertions(+), 15 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index 32c6045..fe9ed78 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -229,6 +229,61 @@ static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
             ( ( ( 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
+ * @param[in] subtrahend
+ *
+ * @return The calculated signed subtraction value between the unsigned integers.
+ */
+static int32_t safeSubtraction( 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 has the most significant bit set.
+     * An unsigned integer with the most significant bit set cannot be safely assigned
+     * to a signed integer.*/
+    if( ( positiveDiff & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK ) == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
+    {
+        /* Perform 2's complement inversion of the value so that the most significant bit
+         * is not set.
+         * Note: This expression is used to  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  - sutrahend". */
+    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.
@@ -339,21 +394,10 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
         int32_t signedFirstOrderDiffSend = 0;
         int32_t signedFirstOrderDiffRecv = 0;
 
-        /* Now we can safely store the first order differences as signed integer values. */
-        signedFirstOrderDiffSend = ( int32_t ) firstOrderDiffSend;
-        signedFirstOrderDiffRecv = ( int32_t ) firstOrderDiffRecv;
-
-        /* To calculate the clock-offset value, we will correct the signed first order difference
-        * values to match the subtraction polarity direction of "Server Time" - "Client Time". */
-        if( sendPolarity == false )
-        {
-            signedFirstOrderDiffSend = 0 - signedFirstOrderDiffSend;
-        }
-
-        if( recvPolarity == false )
-        {
-            signedFirstOrderDiffRecv = 0 - signedFirstOrderDiffRecv;
-        }
+        /* 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 = safeSubtraction( pServerRxTime->seconds, pClientTxTime->seconds );
+        signedFirstOrderDiffRecv = safeSubtraction( 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.

From 0c777b4a0662dc9d1b5d6b1b98a2ce7e311e9fa2 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 23:36:09 +0000
Subject: [PATCH 11/17] More simplification in clock offset calculation
 function

---
 source/core_sntp_serializer.c | 54 ++++++++++++-----------------------
 1 file changed, 18 insertions(+), 36 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index fe9ed78..0d5805c 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -121,18 +121,6 @@
  */
 #define CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK    ( 0xC0000000U )
 
-/**
- * @brief The bit mask for the most-significant bit in an unsigned 32 bit integer.
- * This value is used in the intermediate conversion of unsigned integer to signed
- * integer for the first order difference values during clock-offset calculation.
- *
- * @note The conversion from unsigned to signed integer of first order difference
- * values uses this macro to check whether assignment of the unsigned value to signed
- * integer will overflow, and accordingly, change the unsigned value to safely perform
- * the conversion.
- */
-#define UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK                ( 0x80000000U )
-
 /**
  * @brief Structure representing an SNTP packet header.
  * For more information on SNTP packet format, refer to
@@ -239,8 +227,8 @@ static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
  *                    AND
  *  * Safe conversion of unsigned integer to signed integer
  *
- * @param[in] minuend
- * @param[in] subtrahend
+ * @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.
  */
@@ -256,14 +244,15 @@ static int32_t safeSubtraction( uint32_t minuend,
     uint32_t positiveDiff = ( polarity == true ) ? minuend - subtrahend :
                             subtrahend - minuend;
 
-    /* Check whether the difference value has the most significant bit set.
-     * An unsigned integer with the most significant bit set cannot be safely assigned
-     * to a signed integer.*/
-    if( ( positiveDiff & UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK ) == UINT32_MOST_SIGNIFICANT_BIT_BIT_MASK )
+    /* Check whether the difference value cannot be represented as a signed
+     * integer without some modification. An unsigned integer with the most significant
+     * bit set cannot be safely assigned to a signed integer.*/
+    if( positiveDiff > INT32_MAX )
     {
-        /* Perform 2's complement inversion of the value so that the most significant bit
-         * is not set.
-         * Note: This expression is used to  compliant with both CBMC and MISRA Rule 10.1.
+        /* 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;
@@ -275,7 +264,7 @@ static int32_t safeSubtraction( uint32_t minuend,
     /* Now safely, store the unsigned value as a signed integer. */
     calculatedValue = positiveDiff;
 
-    /* Restore the difference value to represent subtraction in the polarity of "minuend  - sutrahend". */
+    /* Restore the difference value to represent subtraction in the polarity of "minuend  - subtrahend". */
     if( polarity == false )
     {
         calculatedValue = 0 - calculatedValue;
@@ -354,7 +343,6 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
     /* Variable for storing the first-order difference between timestamps. */
     uint32_t firstOrderDiffSend = 0;
     uint32_t firstOrderDiffRecv = 0;
-    bool sendPolarity, recvPolarity;
 
     assert( pClientTxTime != NULL );
     assert( pServerRxTime != NULL );
@@ -362,23 +350,17 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
     assert( pClientRxTime != NULL );
     assert( pClockOffset != NULL );
 
-    /* On-wire protocol formula's polarity for first order difference in the send network
-     * path is T2 (Server Rx) - T1 (Client Tx) .*/
-    sendPolarity = ( pServerRxTime->seconds >= pClientTxTime->seconds ) ? true : false;
-
-    /* On-wire protocol formula's polarity for first order difference in the receive network
-     * path is T3 (Server Tx) - T4 (Client Rx) .*/
-    recvPolarity = ( pServerTxTime->seconds >= pClientRxTime->seconds ) ? true : false;
-
     /* 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 difference
-     * values in the unsigned integer now, and later store the values with correct polarity
-     * (according to the formula) later. */
-    firstOrderDiffSend = sendPolarity ? ( pServerRxTime->seconds - pClientTxTime->seconds ) :
+    /* 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 = recvPolarity ? ( pServerTxTime->seconds - pClientRxTime->seconds ) :
+    firstOrderDiffRecv = ( pServerTxTime->seconds >= pClientRxTime->seconds ) ?
+                         ( pServerTxTime->seconds - pClientRxTime->seconds ) :
                          ( pClientRxTime->seconds - pServerTxTime->seconds );
 
     /* Determine from the first order differences if the system time is within

From 7ad69d4ee940f2e25593c8afc0dc606003cbe1ee Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 13 May 2021 23:55:42 +0000
Subject: [PATCH 12/17] Rename function to be more expressive

---
 source/core_sntp_serializer.c | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index 0d5805c..ab709ac 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -232,8 +232,8 @@ static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
  *
  * @return The calculated signed subtraction value between the unsigned integers.
  */
-static int32_t safeSubtraction( uint32_t minuend,
-                                uint32_t subtrahend )
+static int32_t safeSignedSubtraction( uint32_t minuend,
+                                      uint32_t subtrahend )
 {
     int32_t calculatedValue = 0;
 
@@ -378,8 +378,8 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
 
         /* 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 = safeSubtraction( pServerRxTime->seconds, pClientTxTime->seconds );
-        signedFirstOrderDiffRecv = safeSubtraction( pServerTxTime->seconds, pClientRxTime->seconds );
+        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.

From ceaf23bb863d92ebeac0d4a0b3b2d86d84984f79 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 14 May 2021 00:03:18 +0000
Subject: [PATCH 13/17] Minor hygiene

---
 source/core_sntp_serializer.c | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index ab709ac..cef9272 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -237,16 +237,15 @@ static int32_t safeSignedSubtraction( uint32_t minuend,
 {
     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. */
+    /* 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. An unsigned integer with the most significant
-     * bit set cannot be safely assigned to a signed integer.*/
+     * integer without some modification.*/
     if( positiveDiff > INT32_MAX )
     {
         /* Perform 2's complement inversion of the value to convert it to a value less

From 0dfa01d4d60dc761d9b499ea49f408ec8453f57e Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Sat, 15 May 2021 00:27:24 +0000
Subject: [PATCH 14/17] Improve readability of
 isEligibleForClockOffsetCalculation

---
 lexicon.txt                   |  1 +
 source/core_sntp_serializer.c | 29 +++++++++++++++++++++++++++--
 2 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/lexicon.txt b/lexicon.txt
index 932efbe..e9d989a 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -86,6 +86,7 @@ numofservers
 oldertime
 org
 origintime
+overflown
 packetsize
 param
 pauthcodesize
diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index cef9272..e7496d8 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -208,13 +208,38 @@ static uint32_t readWordFromNetworkByteOrderMemory( const uint32_t * ptr )
  */
 static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
 {
+    /* Thee are 2 cases to cover when checking that the first order difference
+     * represents server and client systems within 34 years of each other.
+     *
+     * 1. When both server and client times are in the same NTP era - This means that
+     *    the passed value of first order difference can be directly used as an NTP timestamp's
+     *    "seconds" representation to determine whether it is more than 34 years in value.
+     *    This can be done by simply checking whether the 2 most significant bits are set.
+     *
+     * 2. When server and client times are in different NTP eras - This means that one
+     *    of the system times has overflown in the NTP value (i.e. represents time after
+     *    7 Feb 2036) while the other system time has not undergone the NTP time overflow.
+     *    For example, when the server time is 0x0000000A and the client time is UINT32_MAX,
+     *    then the passed first order difference value is (UINT32_MAX - 0x0000000A = 0xFFFFFFF5).
+     *    In this example, the actual first order difference is 11 seconds, which is obtained by
+     *    performing a 2's complement inversion on the passed first order difference value i.e.
+     *                Negation of 0xFFFFFFF5 in 32 bits = -0xFFFFFFF5
+     *                                                  = ~0xFFFFFFF5 + 1U
+     *                                                  = UINT32_MAX - 0xFFFFFFF5 + 1U
+     *                                                  = 0x000000F5
+     */
+    bool sameNtpEraCheck = ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ?
+                           true : false;
+
     /* 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 ) );
+    bool diffNtpEraCheck = ( ( ( UINT32_MAX - firstOrderDiff + 1U )
+                               & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ? true : false;
+
+    return( sameNtpEraCheck || diffNtpEraCheck );
 }
 
 /**

From c06675b3a67f6bf9ccc37a89830274a4fd339529 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Mon, 17 May 2021 18:50:42 +0000
Subject: [PATCH 15/17] Rename subtraction utility function and add comments
 for clarification

---
 lexicon.txt                   |  1 +
 source/core_sntp_serializer.c | 65 ++++++++++++++++++++---------------
 2 files changed, 39 insertions(+), 27 deletions(-)

diff --git a/lexicon.txt b/lexicon.txt
index e9d989a..8342435 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -106,6 +106,7 @@ pnetworkcontext
 pnetworkcontext
 pnetworkintf
 poldertime
+positivediff
 posix
 ppacket
 pparsedresponse
diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index e7496d8..3d16750 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -226,7 +226,8 @@ static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
      *                Negation of 0xFFFFFFF5 in 32 bits = -0xFFFFFFF5
      *                                                  = ~0xFFFFFFF5 + 1U
      *                                                  = UINT32_MAX - 0xFFFFFFF5 + 1U
-     *                                                  = 0x000000F5
+     *                                                  = 0x0000000B
+     *                                                  = 11 seconds
      */
     bool sameNtpEraCheck = ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ?
                            true : false;
@@ -243,40 +244,50 @@ static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
 }
 
 /**
- * @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 ).
+ * @brief Utility to safely calculate difference between server and client timestamps of
+ * unsigned integer type and return the value as a signed integer. The calculated value
+ * represents the effective subtraction as ( @p serverTime - @p clientTime ).
  *
- * @note This utility provides safe subtraction result that involve the following 2 operations::
- *  * Safe subtraction between unsigned integers
+ * @note This utility ASSUMES that the timestamps are within 34 years of each other.
+ *
+ * @note This utility provides safe subtraction between unsigned integers that involve the
+ * following 2 operations::
+ *  * Safe subtraction between unsigned integers (to avoid overflow of storing negative value
+ *    in unsigned integer)
  *                    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.
+ * @param[in] serverTime The "seconds" part of the server timestamp.
+ * @param[in] clientTime The "seconds" part of the client timestamp.
  *
- * @return The calculated signed subtraction value between the unsigned integers.
+ * @return The calculated difference value between the server and client timestamps.
  */
-static int32_t safeSignedSubtraction( uint32_t minuend,
-                                      uint32_t subtrahend )
+static int32_t safeTimeDiff( uint32_t serverTime,
+                             uint32_t clientTime )
 {
-    int32_t calculatedValue = 0;
+    int32_t calculatedTimeDiff = 0;
 
-    /* The correct polarity of subtraction is "minuend - subtrahend"
+    /* The correct polarity of subtraction is "Server Time - Client Time"
      * 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.*/
+    bool polarity = ( serverTime > clientTime ) ? true : false;
+    uint32_t positiveDiff = ( polarity == true ) ? serverTime - clientTime :
+                            clientTime - serverTime;
+
+    /* Check whether the difference value cannot be stored as a signed 32 bit integer
+     * as-is due to overflow. If there is overflow, the value will have to be modified
+     * to be represented as signed 32-bit integer.
+     * Note: As we know that the server and client timestamps are within 34 years of
+     * each other, an overflown time difference represents the case when server and client timestamps
+     * are in different NTP eras. Thus, a time difference that overflows is an acceptable
+     * value for this utility.
+     */
     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.
+         * Note: The following expression (UINT32_MAX - positiveDiff + 1U) is used for
+         * 2's complement negation 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;
@@ -286,15 +297,15 @@ static int32_t safeSignedSubtraction( uint32_t minuend,
     }
 
     /* Now safely, store the unsigned value as a signed integer. */
-    calculatedValue = positiveDiff;
+    calculatedTimeDiff = positiveDiff;
 
-    /* Restore the difference value to represent subtraction in the polarity of "minuend  - subtrahend". */
+    /* Restore the difference value to represent subtraction in the polarity of "Server Time - Client Time". */
     if( polarity == false )
     {
-        calculatedValue = 0 - calculatedValue;
+        calculatedTimeDiff = 0 - calculatedTimeDiff;
     }
 
-    return calculatedValue;
+    return calculatedTimeDiff;
 }
 
 /**
@@ -402,8 +413,8 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime,
 
         /* 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 );
+        signedFirstOrderDiffSend = safeTimeDiff( pServerRxTime->seconds, pClientTxTime->seconds );
+        signedFirstOrderDiffRecv = safeTimeDiff( 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.

From 96e663d337a5f94d3adc291653c25c785bc6364b Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Mon, 17 May 2021 23:32:32 +0000
Subject: [PATCH 16/17] Refactor safeTimeDiff function to be more expressive

---
 lexicon.txt                                 |  3 +
 source/core_sntp_serializer.c               | 71 ++++++++++++---------
 test/unit-test/core_sntp_serializer_utest.c | 29 ++++++++-
 3 files changed, 73 insertions(+), 30 deletions(-)

diff --git a/lexicon.txt b/lexicon.txt
index 8342435..f1e9b12 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -1,3 +1,4 @@
+actualabsdiff
 aes
 alarmservernotsynchronized
 api
@@ -37,6 +38,7 @@ deserialize
 deserializer
 deserializeresponse
 desiredaccuracy
+diff
 dns
 doxygen
 endian
@@ -163,6 +165,7 @@ servernamelen
 serverport
 serverresponsetimeoutms
 servertime
+servertxtime
 setsystemtimefunc
 signedfirstorderdiffrecv
 signedfirstorderdiffsend
diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index 3d16750..79d0978 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -267,42 +267,55 @@ static int32_t safeTimeDiff( uint32_t serverTime,
 {
     int32_t calculatedTimeDiff = 0;
 
-    /* The correct polarity of subtraction is "Server Time - Client Time"
-     * but to avoid overflow in subtraction of unsigned integers, we perform
-     * subtraction in the polarity that generates a positive value. */
-    bool polarity = ( serverTime > clientTime ) ? true : false;
-    uint32_t positiveDiff = ( polarity == true ) ? serverTime - clientTime :
-                            clientTime - serverTime;
-
-    /* Check whether the difference value cannot be stored as a signed 32 bit integer
-     * as-is due to overflow. If there is overflow, the value will have to be modified
-     * to be represented as signed 32-bit integer.
+    /* First calculate the difference in 64 bit-width to store any overflow values
+     * from subtraction on 32 bit integer values.*/
+    int64_t diffIn64Bits = ( int64_t ) serverTime - ( int64_t ) clientTime;
+
+    /* Check whether the difference value has overflow for a signed 32 bit integer
+     * If there is overflow, the value will have to be modified before storing it as signed
+     * 32-bit integer.
      * Note: As we know that the server and client timestamps are within 34 years of
-     * each other, an overflown time difference represents the case when server and client timestamps
-     * are in different NTP eras. Thus, a time difference that overflows is an acceptable
-     * value for this utility.
+     * each other, an overflown time difference represents the case when server and
+     * client timestamps are in different NTP eras. Thus, a time difference that overflows is
+     * an acceptable value for this utility.
+     */
+
+    /* Check whether an overflow occurs when the server time is ahead of the client time.
+     * Note: This means that the server time is in NTP era 1 (i.e. after 7 Feb 2036) whereas
+     * client time is in NTP era 0.
      */
-    if( positiveDiff > INT32_MAX )
+    if( diffIn64Bits < INT32_MIN )
     {
-        /* Perform 2's complement inversion of the value to convert it to a value less
-         * than INT32_MAX.
-         * Note: The following expression (UINT32_MAX - positiveDiff + 1U) is used for
-         * 2's complement negation 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;
+        /* Calculate the actual difference in time between the server and client keeping
+         * the different eras in consideration. */
+        uint32_t diff = ( UINT32_MAX - clientTime ) /* Time from client time to end of NTP era 0.*/
+                        + 1U                        /* Time at epoch of NTP era 1, i.e. & Feb 2036 6h:28m:16s UTC */
+                        + serverTime;               /* Time period after NTP era 1. */
+
+        /* Perform 2's complement negation of the absolute difference value to represent
+         * the true time difference between server and client timestamps that are in
+         * different eras. */
+        calculatedTimeDiff = ( int32_t ) diff;
     }
 
-    /* Now safely, store the unsigned value as a signed integer. */
-    calculatedTimeDiff = positiveDiff;
+    /* Check whether overflow occurs when the client time is ahead of the server time.
+     * Note: In this case, the client time would have overflown in NTP era 1 while
+     */
+    else if( diffIn64Bits > INT32_MAX )
+    {
+        /* Calculate the actual difference in time between the server and client keeping
+         * the different eras in consideration. */
+        uint32_t actualAbsDiff = ( UINT32_MAX - serverTime ) /* Time from sever time to end of NTP era 0.*/
+                                 + 1U                        /* Time at epoch of NTP era 1, i.e. & Feb 2036 6h:28m:16s UTC */
+                                 + clientTime;               /* Time period after NTP era 1. */
 
-    /* Restore the difference value to represent subtraction in the polarity of "Server Time - Client Time". */
-    if( polarity == false )
+        calculatedTimeDiff = 0 - ( int32_t ) actualAbsDiff;
+    }
+    else
     {
-        calculatedTimeDiff = 0 - calculatedTimeDiff;
+        /* We are confident that the time difference value can be represented as a signed
+         * 32 bit integer. */
+        calculatedTimeDiff = ( int32_t ) diffIn64Bits;
     }
 
     return calculatedTimeDiff;
diff --git a/test/unit-test/core_sntp_serializer_utest.c b/test/unit-test/core_sntp_serializer_utest.c
index 5e30f99..55c55dd 100644
--- a/test/unit-test/core_sntp_serializer_utest.c
+++ b/test/unit-test/core_sntp_serializer_utest.c
@@ -137,6 +137,9 @@ static void testClockOffsetCalculation( SntpTimestamp_t * clientTxTime,
                                         int32_t expectedClockOffset )
 {
     /* Update the response packet with the server time. */
+    addTimestampToResponseBuffer( clientTxTime,
+                                  testBuffer,
+                                  SNTP_PACKET_ORIGIN_TIME_FIRST_BYTE_POS );
     addTimestampToResponseBuffer( serverRxTime,
                                   testBuffer,
                                   SNTP_PACKET_RX_TIMESTAMP_FIRST_BYTE_POS );
@@ -498,6 +501,8 @@ void test_DeserializeResponse_AcceptedResponse_Nominal_Case( void )
     /* Use the the same values for Rx and Tx times for server and client in the first couple
      * of tests for simplicity. */
 
+    /* ==================Test when client and server are in same NTP era.================ */
+
     /* Test when the client is 20 years ahead of server time to generate a negative offset
      * result.*/
     SntpTimestamp_t serverTxTime =
@@ -513,9 +518,30 @@ void test_DeserializeResponse_AcceptedResponse_Nominal_Case( void )
 
     /* Now test for the client being 20 years behind server time to generate a positive
      * offset result.*/
-    serverTxTime.seconds = clientTxTime.seconds + YEARS_20_IN_SECONDS;
+    serverTxTime.seconds = UINT32_MAX;
+    clientTxTime.seconds = UINT32_MAX - YEARS_20_IN_SECONDS;
     expectedOffset = YEARS_20_IN_SECONDS;
 
+    testClockOffsetCalculation( &clientTxTime, &serverTxTime,
+                                &serverTxTime, &clientTxTime,
+                                SntpSuccess, expectedOffset );
+
+    /* ==================Test when client and server are in different NTP eras.================ */
+
+    /* Test when the server is ahead of client to generate a positive clock offset result.*/
+    clientTxTime.seconds = UINT32_MAX;                       /* Client is in NTP era 0. */
+    serverTxTime.seconds = UINT32_MAX + YEARS_20_IN_SECONDS; /* Server is in NTP era 1. */
+    expectedOffset = YEARS_20_IN_SECONDS;
+
+    testClockOffsetCalculation( &clientTxTime, &serverTxTime,
+                                &serverTxTime, &clientTxTime,
+                                SntpSuccess, expectedOffset );
+
+    /* Test when the client is ahead of server to generate a negative clock offset result.*/
+    clientTxTime.seconds = UINT32_MAX + YEARS_20_IN_SECONDS; /* Client is in NTP era 1. */
+    serverTxTime.seconds = UINT32_MAX;                       /* Server is in NTP era 0. */
+    expectedOffset = -YEARS_20_IN_SECONDS;
+
     testClockOffsetCalculation( &clientTxTime, &serverTxTime,
                                 &serverTxTime, &clientTxTime,
                                 SntpSuccess, expectedOffset );
@@ -524,6 +550,7 @@ void test_DeserializeResponse_AcceptedResponse_Nominal_Case( void )
      * that are used in the clock-offset calculation.
      * The test case uses 2 seconds as network delay on both Client -> Server and Server -> Client path
      * and 2 seconds for server processing time between receiving SNTP request and sending SNTP response */
+    clientTxTime.seconds = UINT32_MAX;
     SntpTimestamp_t serverRxTime =
     {
         clientTxTime.seconds + YEARS_20_IN_SECONDS + 2,

From bcb4dfc8409fe9d759508b20f51afc806cb9f60d Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Mon, 17 May 2021 23:43:22 +0000
Subject: [PATCH 17/17] Fix overflow issue in
 isEligibleForClockOffsetCalculation function

---
 source/core_sntp_serializer.c | 31 +++++++++++++++++++++----------
 1 file changed, 21 insertions(+), 10 deletions(-)

diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c
index 79d0978..527e3bb 100644
--- a/source/core_sntp_serializer.c
+++ b/source/core_sntp_serializer.c
@@ -229,16 +229,27 @@ static bool isEligibleForClockOffsetCalculation( uint32_t firstOrderDiff )
      *                                                  = 0x0000000B
      *                                                  = 11 seconds
      */
-    bool sameNtpEraCheck = ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ?
-                           true : false;
-
-    /* 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. */
-    bool diffNtpEraCheck = ( ( ( UINT32_MAX - firstOrderDiff + 1U )
-                               & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ? true : false;
+    bool sameNtpEraCheck = false;
+    bool diffNtpEraCheck = false;
+
+    /* Check if the server and client times are within 34 years of each other, if we assume that they are
+     * in the same NTP era. */
+    sameNtpEraCheck = ( ( firstOrderDiff & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ?
+                      true : false;
+
+    /* If the same era check does not satisfy the 34 years condition, check
+     * whether the condition is satisfied when assuming the that the systems are in
+     * different NTP eras. */
+    if( sameNtpEraCheck == false )
+    {
+        /* 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. */
+        diffNtpEraCheck = ( ( ( UINT32_MAX - firstOrderDiff + 1U )
+                              & CLOCK_OFFSET_FIRST_ORDER_DIFF_OVERFLOW_BITS_MASK ) == 0U ) ? true : false;
+    }
 
     return( sameNtpEraCheck || diffNtpEraCheck );
 }