From 6f2017e9deeb3becd714ba1ba1a1596f180055ad Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 29 Apr 2021 16:36:53 -0700 Subject: [PATCH 01/44] Set up litani infra for coreSNTP --- test/cbmc/.gitignore | 23 ++ test/cbmc/include/README.md | 1 + test/cbmc/negative_tests/README.md | 1 + test/cbmc/negative_tests/assert/Makefile | 1 + .../negative_tests/assert/assert_harness.c | 1 + .../cbmc/negative_tests/bounds_check/Makefile | 1 + .../bounds_check/bounds_check_harness.c | 1 + .../negative_tests/conversion_check/Makefile | 1 + .../conversion_check_harness.c | 1 + .../negative_tests/div_by_zero_check/Makefile | 1 + .../div_by_zero_check_harness.c | 1 + .../float_overflow_check/Makefile | 1 + .../float_overflow_check_harness.c | 1 + .../float_underflow_check/Makefile | 1 + .../float_underflow_check_harness.c | 1 + test/cbmc/negative_tests/nan_check/Makefile | 1 + .../nan_check/nan_check_harness.c | 1 + .../negative_tests/pointer_check/Makefile | 1 + .../pointer_check/pointer_check_harness.c | 1 + .../pointer_overflow_check/Makefile | 1 + .../pointer_overflow_check_harness.c | 1 + .../pointer_primitive_check/Makefile | 1 + .../pointer_primitive_check_harness.c | 1 + .../pointer_underflow_check/Makefile | 1 + .../pointer_underflow_check_harness.c | 1 + .../signed_overflow_check/Makefile | 1 + .../signed_overflow_check_harness.c | 1 + .../signed_underflow_check/Makefile | 1 + .../signed_underflow_check_harness.c | 1 + .../undefined_shift_check/Makefile | 1 + .../undefined_shift_check_harness.c | 1 + .../unsigned_overflow_check/Makefile | 1 + .../unsigned_overflow_check_harness.c | 1 + .../unsigned_underflow_check/Makefile | 1 + .../unsigned_underflow_check_harness.c | 1 + test/cbmc/proofs/Makefile-project-defines | 37 +++ test/cbmc/proofs/Makefile-project-targets | 10 + test/cbmc/proofs/Makefile-project-testing | 11 + test/cbmc/proofs/Makefile-template-defines | 19 ++ test/cbmc/proofs/Makefile.common | 1 + test/cbmc/proofs/README.md | 1 + test/cbmc/proofs/prepare.py | 1 + test/cbmc/proofs/run-cbmc-proofs.py | 259 ++++++++++++++++++ test/cbmc/sources/README.md | 1 + test/cbmc/stubs/README.md | 1 + 45 files changed, 398 insertions(+) create mode 100644 test/cbmc/.gitignore create mode 120000 test/cbmc/include/README.md create mode 120000 test/cbmc/negative_tests/README.md create mode 120000 test/cbmc/negative_tests/assert/Makefile create mode 120000 test/cbmc/negative_tests/assert/assert_harness.c create mode 120000 test/cbmc/negative_tests/bounds_check/Makefile create mode 120000 test/cbmc/negative_tests/bounds_check/bounds_check_harness.c create mode 120000 test/cbmc/negative_tests/conversion_check/Makefile create mode 120000 test/cbmc/negative_tests/conversion_check/conversion_check_harness.c create mode 120000 test/cbmc/negative_tests/div_by_zero_check/Makefile create mode 120000 test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c create mode 120000 test/cbmc/negative_tests/float_overflow_check/Makefile create mode 120000 test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c create mode 120000 test/cbmc/negative_tests/float_underflow_check/Makefile create mode 120000 test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c create mode 120000 test/cbmc/negative_tests/nan_check/Makefile create mode 120000 test/cbmc/negative_tests/nan_check/nan_check_harness.c create mode 120000 test/cbmc/negative_tests/pointer_check/Makefile create mode 120000 test/cbmc/negative_tests/pointer_check/pointer_check_harness.c create mode 120000 test/cbmc/negative_tests/pointer_overflow_check/Makefile create mode 120000 test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c create mode 120000 test/cbmc/negative_tests/pointer_primitive_check/Makefile create mode 120000 test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c create mode 120000 test/cbmc/negative_tests/pointer_underflow_check/Makefile create mode 120000 test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c create mode 120000 test/cbmc/negative_tests/signed_overflow_check/Makefile create mode 120000 test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c create mode 120000 test/cbmc/negative_tests/signed_underflow_check/Makefile create mode 120000 test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c create mode 120000 test/cbmc/negative_tests/undefined_shift_check/Makefile create mode 120000 test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c create mode 120000 test/cbmc/negative_tests/unsigned_overflow_check/Makefile create mode 120000 test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c create mode 120000 test/cbmc/negative_tests/unsigned_underflow_check/Makefile create mode 120000 test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c create mode 100644 test/cbmc/proofs/Makefile-project-defines create mode 100644 test/cbmc/proofs/Makefile-project-targets create mode 100644 test/cbmc/proofs/Makefile-project-testing create mode 100644 test/cbmc/proofs/Makefile-template-defines create mode 120000 test/cbmc/proofs/Makefile.common create mode 120000 test/cbmc/proofs/README.md create mode 120000 test/cbmc/proofs/prepare.py create mode 100644 test/cbmc/proofs/run-cbmc-proofs.py create mode 120000 test/cbmc/sources/README.md create mode 120000 test/cbmc/stubs/README.md diff --git a/test/cbmc/.gitignore b/test/cbmc/.gitignore new file mode 100644 index 0000000..44240c2 --- /dev/null +++ b/test/cbmc/.gitignore @@ -0,0 +1,23 @@ +# Emitted when running CBMC proofs +proofs/**/logs +proofs/**/gotos +proofs/**/report +proofs/**/html + +# Emitted by CBMC Viewer +TAGS-* + +# Emitted by Arpa +arpa_cmake/ +arpa-validation-logs/ +Makefile.arpa + +# Emitted by litani +.ninja_deps +.ninja_log +.litani_cache_dir + +# These files should be overwritten whenever prepare.py runs +cbmc-batch.yaml + +__pycache__/ diff --git a/test/cbmc/include/README.md b/test/cbmc/include/README.md new file mode 120000 index 0000000..4086b9e --- /dev/null +++ b/test/cbmc/include/README.md @@ -0,0 +1 @@ +../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md \ No newline at end of file diff --git a/test/cbmc/negative_tests/README.md b/test/cbmc/negative_tests/README.md new file mode 120000 index 0000000..60e8d6c --- /dev/null +++ b/test/cbmc/negative_tests/README.md @@ -0,0 +1 @@ +../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/README.md \ No newline at end of file diff --git a/test/cbmc/negative_tests/assert/Makefile b/test/cbmc/negative_tests/assert/Makefile new file mode 120000 index 0000000..f5dc5cb --- /dev/null +++ b/test/cbmc/negative_tests/assert/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/assert/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/assert/assert_harness.c b/test/cbmc/negative_tests/assert/assert_harness.c new file mode 120000 index 0000000..4405e98 --- /dev/null +++ b/test/cbmc/negative_tests/assert/assert_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/assert/assert_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/bounds_check/Makefile b/test/cbmc/negative_tests/bounds_check/Makefile new file mode 120000 index 0000000..da823de --- /dev/null +++ b/test/cbmc/negative_tests/bounds_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/bounds_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/bounds_check/bounds_check_harness.c b/test/cbmc/negative_tests/bounds_check/bounds_check_harness.c new file mode 120000 index 0000000..5b01436 --- /dev/null +++ b/test/cbmc/negative_tests/bounds_check/bounds_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/bounds_check/bounds_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/conversion_check/Makefile b/test/cbmc/negative_tests/conversion_check/Makefile new file mode 120000 index 0000000..238306b --- /dev/null +++ b/test/cbmc/negative_tests/conversion_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/conversion_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/conversion_check/conversion_check_harness.c b/test/cbmc/negative_tests/conversion_check/conversion_check_harness.c new file mode 120000 index 0000000..44e9e2c --- /dev/null +++ b/test/cbmc/negative_tests/conversion_check/conversion_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/conversion_check/conversion_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/div_by_zero_check/Makefile b/test/cbmc/negative_tests/div_by_zero_check/Makefile new file mode 120000 index 0000000..98362b7 --- /dev/null +++ b/test/cbmc/negative_tests/div_by_zero_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/div_by_zero_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c b/test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c new file mode 120000 index 0000000..9351146 --- /dev/null +++ b/test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/div_by_zero_check/div_by_zero_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/float_overflow_check/Makefile b/test/cbmc/negative_tests/float_overflow_check/Makefile new file mode 120000 index 0000000..8a694fc --- /dev/null +++ b/test/cbmc/negative_tests/float_overflow_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_overflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c b/test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c new file mode 120000 index 0000000..b0b7c8b --- /dev/null +++ b/test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_overflow_check/float_overflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/float_underflow_check/Makefile b/test/cbmc/negative_tests/float_underflow_check/Makefile new file mode 120000 index 0000000..a92febc --- /dev/null +++ b/test/cbmc/negative_tests/float_underflow_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_underflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c b/test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c new file mode 120000 index 0000000..ff99ec6 --- /dev/null +++ b/test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_underflow_check/float_underflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/nan_check/Makefile b/test/cbmc/negative_tests/nan_check/Makefile new file mode 120000 index 0000000..4a967a5 --- /dev/null +++ b/test/cbmc/negative_tests/nan_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/nan_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/nan_check/nan_check_harness.c b/test/cbmc/negative_tests/nan_check/nan_check_harness.c new file mode 120000 index 0000000..f2e73cb --- /dev/null +++ b/test/cbmc/negative_tests/nan_check/nan_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/nan_check/nan_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_check/Makefile b/test/cbmc/negative_tests/pointer_check/Makefile new file mode 120000 index 0000000..1134103 --- /dev/null +++ b/test/cbmc/negative_tests/pointer_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_check/pointer_check_harness.c b/test/cbmc/negative_tests/pointer_check/pointer_check_harness.c new file mode 120000 index 0000000..c16774a --- /dev/null +++ b/test/cbmc/negative_tests/pointer_check/pointer_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_check/pointer_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_overflow_check/Makefile b/test/cbmc/negative_tests/pointer_overflow_check/Makefile new file mode 120000 index 0000000..cadcbe8 --- /dev/null +++ b/test/cbmc/negative_tests/pointer_overflow_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_overflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c b/test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c new file mode 120000 index 0000000..e1ed818 --- /dev/null +++ b/test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_primitive_check/Makefile b/test/cbmc/negative_tests/pointer_primitive_check/Makefile new file mode 120000 index 0000000..7b01588 --- /dev/null +++ b/test/cbmc/negative_tests/pointer_primitive_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_primitive_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c b/test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c new file mode 120000 index 0000000..6c2e2dc --- /dev/null +++ b/test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_underflow_check/Makefile b/test/cbmc/negative_tests/pointer_underflow_check/Makefile new file mode 120000 index 0000000..b05fce3 --- /dev/null +++ b/test/cbmc/negative_tests/pointer_underflow_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_underflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c b/test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c new file mode 120000 index 0000000..06b831d --- /dev/null +++ b/test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/signed_overflow_check/Makefile b/test/cbmc/negative_tests/signed_overflow_check/Makefile new file mode 120000 index 0000000..5b1e6e1 --- /dev/null +++ b/test/cbmc/negative_tests/signed_overflow_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_overflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c b/test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c new file mode 120000 index 0000000..fd74c10 --- /dev/null +++ b/test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_overflow_check/signed_overflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/signed_underflow_check/Makefile b/test/cbmc/negative_tests/signed_underflow_check/Makefile new file mode 120000 index 0000000..ed10e0a --- /dev/null +++ b/test/cbmc/negative_tests/signed_underflow_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_underflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c b/test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c new file mode 120000 index 0000000..0835085 --- /dev/null +++ b/test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_underflow_check/signed_underflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/undefined_shift_check/Makefile b/test/cbmc/negative_tests/undefined_shift_check/Makefile new file mode 120000 index 0000000..f6c2cd2 --- /dev/null +++ b/test/cbmc/negative_tests/undefined_shift_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/undefined_shift_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c b/test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c new file mode 120000 index 0000000..f4dbf13 --- /dev/null +++ b/test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/undefined_shift_check/undefined_shift_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/unsigned_overflow_check/Makefile b/test/cbmc/negative_tests/unsigned_overflow_check/Makefile new file mode 120000 index 0000000..41fa254 --- /dev/null +++ b/test/cbmc/negative_tests/unsigned_overflow_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_overflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c b/test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c new file mode 120000 index 0000000..a0359f9 --- /dev/null +++ b/test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/unsigned_underflow_check/Makefile b/test/cbmc/negative_tests/unsigned_underflow_check/Makefile new file mode 120000 index 0000000..e0fc5c4 --- /dev/null +++ b/test/cbmc/negative_tests/unsigned_underflow_check/Makefile @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_underflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c b/test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c new file mode 120000 index 0000000..949db40 --- /dev/null +++ b/test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c @@ -0,0 +1 @@ +../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines new file mode 100644 index 0000000..f6f7681 --- /dev/null +++ b/test/cbmc/proofs/Makefile-project-defines @@ -0,0 +1,37 @@ +# -*- mode: makefile -*- +# The first line sets the emacs major mode to Makefile + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +################################################################ +# Use this file to give project-specific definitions of the command +# line arguments to pass to CBMC tools like goto-cc to build the goto +# binaries and cbmc to do the property and coverage checking. +# +# Use this file to override most default definitions of variables in +# Makefile.common. +################################################################ + +# Flags to pass to goto-cc for compilation (typically those passed to gcc -c) +# COMPILE_FLAGS = + +# Flags to pass to goto-cc for linking (typically those passed to gcc) +# LINK_FLAGS = + +# Preprocessor include paths -I... +# Consider adding +# INCLUDES += -I$(CBMC_ROOT)/include +# You will want to decide what order that comes in relative to the other +# include directories in your project. +# +# INCLUDES = + +# Preprocessor definitions -D... +# DEFINES = + +# Path to arpa executable +# ARPA = + +# Flags to pass to cmake for building the project +# ARPA_CMAKE_FLAGS = diff --git a/test/cbmc/proofs/Makefile-project-targets b/test/cbmc/proofs/Makefile-project-targets new file mode 100644 index 0000000..2d4d460 --- /dev/null +++ b/test/cbmc/proofs/Makefile-project-targets @@ -0,0 +1,10 @@ +# -*- mode: makefile -*- +# The first line sets the emacs major mode to Makefile + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +################################################################ +# Use this file to give project-specific targets, including targets +# that may depend on targets defined in Makefile.common. +################################################################ diff --git a/test/cbmc/proofs/Makefile-project-testing b/test/cbmc/proofs/Makefile-project-testing new file mode 100644 index 0000000..dc0c209 --- /dev/null +++ b/test/cbmc/proofs/Makefile-project-testing @@ -0,0 +1,11 @@ +# -*- mode: makefile -*- +# The first line sets the emacs major mode to Makefile + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +################################################################ +# Use this file to define project-specific targets and definitions for +# unit testing or continuous integration that may depend on targets +# defined in Makefile.common +################################################################ diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines new file mode 100644 index 0000000..0ceb406 --- /dev/null +++ b/test/cbmc/proofs/Makefile-template-defines @@ -0,0 +1,19 @@ + +# Absolute path to the root of the source tree. +# +SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../source) + + +# Absolute path to the litani script. +# +LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani) + + +# Name of this proof project, displayed in proof reports. For example, +# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots, +# this may be overridden on the command-line to Make, for example +# +# make PROJECT_NAME="FreeRTOS MQTT" report +# +PROJECT_NAME = "coreSNTP" + diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common new file mode 120000 index 0000000..69d247e --- /dev/null +++ b/test/cbmc/proofs/Makefile.common @@ -0,0 +1 @@ +../aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common \ No newline at end of file diff --git a/test/cbmc/proofs/README.md b/test/cbmc/proofs/README.md new file mode 120000 index 0000000..cac5275 --- /dev/null +++ b/test/cbmc/proofs/README.md @@ -0,0 +1 @@ +../aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md \ No newline at end of file diff --git a/test/cbmc/proofs/prepare.py b/test/cbmc/proofs/prepare.py new file mode 120000 index 0000000..97c77e9 --- /dev/null +++ b/test/cbmc/proofs/prepare.py @@ -0,0 +1 @@ +../aws-templates-for-cbmc-proofs/template-for-repository/proofs/prepare.py \ No newline at end of file diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py new file mode 100644 index 0000000..2a60ab0 --- /dev/null +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -0,0 +1,259 @@ +#!/usr/bin/env python3 +# +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + + +import argparse +import asyncio +import logging +import math +import os +import pathlib +import subprocess +import sys + + +DESCRIPTION = "Configure and run all CBMC proofs in parallel" + +# Keep the epilog hard-wrapped at 70 characters, as it gets printed +# verbatim in the terminal. 70 characters stops here --------------> | +EPILOG = """ +This tool automates the process of running `make report` in each of +the CBMC proof directories. The tool calculates the dependency graph +of all tasks needed to build, run, and report on all the proofs, and +executes these tasks in parallel. + +The tool is roughly equivalent to doing this: + + litani init --project "my-cool-project"; + + find . -name cbmc-proof.txt | while read -r proof; do + pushd $(dirname ${proof}); + + # The `make _report` rule adds a single proof to litani + # without running it + make _report; + + popd; + done + + litani run-build; + +except that it is much faster and provides some convenience options. +The CBMC CI runs this script with no arguments to build and run all +proofs in parallel. The value of "my-cool-project" is taken from the +PROJECT_NAME variable in Makefile-project-defines. + +The --no-standalone argument omits the `litani init` and `litani +run-build`; use it when you want to add additional proof jobs, not +just the CBMC ones. In that case, you would run `litani init` +yourself; then run `run-cbmc-proofs --no-standalone`; add any +additional jobs that you want to execute with `litani add-job`; and +finally run `litani run-build`. +""" + + +def get_project_name(): + cmd = [ + "make", + "-f", "Makefile.common", + "echo-project-name", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) + if proc.returncode: + logging.critical("could not run make to determine project name") + sys.exit(1) + if not proc.stdout.strip(): + logging.warning( + "project name has not been set; using generic name instead. " + "Set the PROJECT_NAME value in Makefile-project-defines to " + "remove this warning") + return "" + return proc.stdout.strip() + + +def get_args(): + pars = argparse.ArgumentParser( + description=DESCRIPTION, epilog=EPILOG, + formatter_class=argparse.RawDescriptionHelpFormatter) + for arg in [{ + "flags": ["-j", "--parallel-jobs"], + "type": int, + "metavar": "N", + "help": "run at most N proof jobs in parallel", + }, { + "flags": ["--no-standalone"], + "action": "store_true", + "help": "only configure proofs: do not initialize nor run", + }, { + "flags": ["-p", "--proofs"], + "nargs": "+", + "metavar": "DIR", + "help": "only run proof in directory DIR (can pass more than one)", + }, { + "flags": ["--project-name"], + "metavar": "NAME", + "default": get_project_name(), + "help": "project name for report. Default: %(default)s", + }, { + "flags": ["--proof-marker"], + "metavar": "FILE", + "default": "cbmc-proof.txt", + "help": ( + "name of file that marks proof directories. Default: " + "%(default)s"), + }, { + "flags": ["--verbose"], + "action": "store_true", + "help": "verbose output", + }]: + flags = arg.pop("flags") + pars.add_argument(*flags, **arg) + return pars.parse_args() + + +def set_up_logging(verbose): + if verbose: + level = logging.DEBUG + else: + level = logging.WARNING + logging.basicConfig( + format="run-cbmc-proofs: %(message)s", level=level) + + +def task_pool_size(): + ret = os.cpu_count() + if ret is None or ret < 3: + return 1 + return ret - 2 + + +def print_counter(counter): + print( + "\rConfiguring CBMC proofs: " + "{complete:{width}} / {total:{width}}".format( + **counter), end="", file=sys.stderr) + + +def get_proof_dirs(proof_root, proof_list, proof_marker): + if proof_list is not None: + proofs_remaining = list(proof_list) + else: + proofs_remaining = [] + + for root, _, fyles in os.walk(proof_root): + proof_name = str(pathlib.Path(root).name) + if proof_list and proof_name not in proof_list: + continue + if proof_list and proof_name in proofs_remaining: + proofs_remaining.remove(proof_name) + if proof_marker in fyles: + yield root + + if proofs_remaining: + logging.critical( + "The following proofs were not found: %s", + ", ".join(proofs_remaining)) + sys.exit(1) + + +def run_build(litani, jobs): + cmd = [str(litani), "run-build"] + if jobs: + cmd.extend(["-j", str(jobs)]) + + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd) + if proc.returncode: + logging.critical("Failed to run litani run-build") + sys.exit(1) + + +def get_litani_path(proof_root): + cmd = [ + "make", + "PROOF_ROOT=%s" % proof_root, + "-f", "Makefile.common", + "litani-path", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) + if proc.returncode: + logging.critical("Could not determine path to litani") + sys.exit(1) + return proc.stdout.strip() + + +async def configure_proof_dirs(queue, counter): + while True: + print_counter(counter) + path = str(await queue.get()) + + proc = await asyncio.create_subprocess_exec( + "nice", "-n", "15", "make", "-B", "--quiet", "_report", cwd=path) + await proc.wait() + counter["fail" if proc.returncode else "pass"].append(path) + counter["complete"] += 1 + + print_counter(counter) + queue.task_done() + + +async def main(): + args = get_args() + set_up_logging(args.verbose) + + proof_root = pathlib.Path(__file__).resolve().parent + litani = get_litani_path(proof_root) + + if not args.no_standalone: + cmd = [str(litani), "init", "--project", args.project_name] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd) + if proc.returncode: + logging.critical("Failed to run litani init") + sys.exit(1) + + proof_dirs = list(get_proof_dirs( + proof_root, args.proofs, args.proof_marker)) + if not proof_dirs: + logging.critical("No proof directories found") + sys.exit(1) + + proof_queue = asyncio.Queue() + for proof_dir in proof_dirs: + proof_queue.put_nowait(proof_dir) + + counter = { + "pass": [], + "fail": [], + "complete": 0, + "total": len(proof_dirs), + "width": int(math.log10(len(proof_dirs))) + 1 + } + + tasks = [] + for _ in range(task_pool_size()): + task = asyncio.create_task(configure_proof_dirs( + proof_queue, counter)) + tasks.append(task) + + await proof_queue.join() + + print_counter(counter) + print("", file=sys.stderr) + + if counter["fail"]: + logging.critical( + "Failed to configure the following proofs:\n%s", "\n".join( + [str(f) for f in counter["fail"]])) + sys.exit(1) + + if not args.no_standalone: + run_build(litani, args.parallel_jobs) + + +if __name__ == "__main__": + asyncio.run(main()) diff --git a/test/cbmc/sources/README.md b/test/cbmc/sources/README.md new file mode 120000 index 0000000..969d1de --- /dev/null +++ b/test/cbmc/sources/README.md @@ -0,0 +1 @@ +../aws-templates-for-cbmc-proofs/template-for-repository/sources/README.md \ No newline at end of file diff --git a/test/cbmc/stubs/README.md b/test/cbmc/stubs/README.md new file mode 120000 index 0000000..327d6f6 --- /dev/null +++ b/test/cbmc/stubs/README.md @@ -0,0 +1 @@ +../aws-templates-for-cbmc-proofs/template-for-repository/stubs/README.md \ No newline at end of file From ec80f3a28d14b5c63ca08e40c410ba74df8964d1 Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Fri, 30 Apr 2021 15:51:26 -0700 Subject: [PATCH 02/44] Add content to README.md (#9) --- .github/workflows/ci.yml | 15 ++++++++++ README.md | 61 +++++++++++++++++++++++++++------------- 2 files changed, 57 insertions(+), 19 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4ba6396..be464e0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -76,3 +76,18 @@ jobs: run: | git-secrets --register-aws git-secrets --scan + link-verifier: + runs-on: ubuntu-18.04 + steps: + - uses: actions/checkout@v2 + - name: Setup Python for link verifier action + uses: actions/setup-python@v2 + with: + python-version: '3.8' + - name: Check Links + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + uses: FreeRTOS/CI-CD-GitHub-Actions/link-verifier@main + with: + path: ./ + include-file-types: .c,.h,.dox diff --git a/README.md b/README.md index e7970a5..d6c42a3 100644 --- a/README.md +++ b/README.md @@ -1,44 +1,67 @@ ## coreSNTP Library -This repository contains the coreSNTP library, a client library to use the Simple Network Time Protocol (SNTP), that is specified in [RFC 4330](https://tools.ietf.org/html/rfc4330), to synchronize client devices with network time. -According to the SNTPv4 specification, "_To an NTP or SNTP server, NTP and SNTP clients are indistinguishable; to an NTP or SNTP client, NTP and SNTP servers are indistinguishable._", thereby, allowing SNTP clients to request time from NTP servers. +**Note:** This library is under development. -## Reference example +This repository contains the coreSNTP library, a client library to use Simple Network Time Protocol (SNTP) to synchronize device clocks with internet time. This library implements the SNTPv4 specification defined in [RFC 4330](https://tools.ietf.org/html/rfc4330). +An SNTP client can request time from both NTP and SNTP servers. According to the SNTPv4 specification, "_To an NTP or SNTP server, NTP and SNTP clients are indistinguishable; to an NTP or SNTP client, NTP and SNTP servers are indistinguishable._", thereby, allowing SNTP clients to request time from NTP servers. + +## Cloning this repository +This repo uses [Git Submodules](https://git-scm.com/book/en/v2/Git-Tools-Submodules) to bring in dependent components. + +To clone using HTTPS: +``` +git clone https://github.com/FreeRTOS/coreSNTP.git --recurse-submodules +``` +Using SSH: +``` +git clone git@github.com:FreeRTOS/coreSNTP.git --recurse-submodules +``` + +If you have downloaded the repo without using the `--recurse-submodules` argument, you need to run: +``` +git submodule update --init --recursive +``` ## Building the library -## Building unit tests +You can build the coreSNTP source files that are in the [source](source/) directory, and add [source/include](source/include) to your compiler's include path. + +If using CMake, the [coreSntpFilePaths.cmake](coreSntpFilePaths.cmake) file contains the above information of the source files and the header include path from this repository. + +## Building Unit Tests -### Checkout Unity Submodule -By default, the submodules in this repository are configured with `update=none` in [.gitmodules](.gitmodules), to avoid increasing clone time and disk space usage of other repositories (like [amazon-freertos](https://github.com/aws/amazon-freertos) that submodules this repository). +### Checkout CMock Submodule -To build unit tests, the submodule dependency of Unity is required. Use the following command to clone the submodule: +To build unit tests, the submodule dependency of CMock is required. Use the following command to clone the submodule: ``` -git submodule update --checkout --init --recursive --test/unit-test/Unity +git submodule update --checkout --init --recursive test/unit-test/CMock ``` -### Platform Prerequisites +### Unit Test Platform Prerequisites - For running unit tests - - C89 or later compiler like gcc - - CMake 3.13.0 or later -- For running the coverage target, gcov is additionally required. + - **C90 compiler** like gcc + - **CMake 3.13.0 or later** + - **Ruby 2.0.0 or later** is additionally required for the CMock test framework (that we use). +- For running the coverage target, **gcov** and **lcov** are additionally required. -### Steps to build Unit Tests +### Steps to build **Unit Tests** -1. Go to the root directory of this repository. (Make sure that the **Unity** submodule is cloned as described [above](#checkout-unity-submodule).) +1. Go to the root directory of this repository. (Make sure that the **CMock** submodule is cloned as described [above](#checkout-cmock-submodule)) -1. Create build directory: `mkdir build && cd build` +1. Run the *cmake* command: `cmake -S test -B build` -1. Run *cmake* while inside build directory: `cmake -S ../test` - -1. Run this command to build the library and unit tests: `make all` +1. Run this command to build the library and unit tests: `make -C build all` 1. The generated test executables will be present in `build/bin/tests` folder. -1. Run `ctest` to execute all tests and view the test run summary. +1. Run `cd build && ctest` to execute all tests and view the test run summary. ## Contributing See [CONTRIBUTING.md](./.github/CONTRIBUTING.md) for information on contributing. + +## License + +This library is licensed under the MIT License. See the [LICENSE](LICENSE) file. From 7d07bee3ee20ba572fb12cb91de8135d616edf15 Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Mon, 3 May 2021 12:47:05 -0700 Subject: [PATCH 03/44] 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. --- coreSntpFilePaths.cmake | 3 +- lexicon.txt | 38 ++ source/core_sntp_client.c | 104 ++++++ source/include/core_sntp_client.h | 474 ++++++++++++++++++++++++ source/include/core_sntp_serializer.h | 24 +- test/CMakeLists.txt | 2 +- test/unit-test/CMakeLists.txt | 11 +- test/unit-test/core_sntp_client_utest.c | 438 ++++++++++++++++++++++ 8 files changed, 1089 insertions(+), 5 deletions(-) create mode 100644 source/core_sntp_client.c create mode 100644 source/include/core_sntp_client.h create mode 100644 test/unit-test/core_sntp_client_utest.c diff --git a/coreSntpFilePaths.cmake b/coreSntpFilePaths.cmake index d44f479..b8e3bd7 100644 --- a/coreSntpFilePaths.cmake +++ b/coreSntpFilePaths.cmake @@ -7,7 +7,8 @@ # coreSNTP library source files. set( CORE_SNTP_SOURCES - "${CMAKE_CURRENT_LIST_DIR}/source/core_sntp_serializer.c" ) + "${CMAKE_CURRENT_LIST_DIR}/source/core_sntp_serializer.c" + "${CMAKE_CURRENT_LIST_DIR}/source/core_sntp_client.c" ) # coreSNTP library Public Include directories. set( CORE_SNTP_INCLUDE_PUBLIC_DIRS diff --git a/lexicon.txt b/lexicon.txt index 686264a..8f7a54d 100644 --- a/lexicon.txt +++ b/lexicon.txt @@ -1,17 +1,27 @@ +aes alarmservernotsynchronized api ascii +auth backoff buffersize +bytestorecv +bytestorecv +bytestosend +bytestosend clienttxtime clockfreqtolerance clockoffsetsec +cmac com +const coresntp de +deamon december deserializeresponse desiredaccuracy +dns endian endif enum @@ -22,6 +32,8 @@ feb fracs fracsinnetorder fracsinnetorder +getsystemtimefunc +getsystemtimefunc gov html htonl @@ -42,15 +54,25 @@ noleapsecond noninfringement ntp ntpv +numofservers org origintime param +pauthcodesize +pauthcodesize +pauthintf +pauthintf pbuffer pclientrxtime pclienttxtime pclockoffset +pcontext pcurrenttime pml +pnetworkbuffer +pnetworkbuffer +pnetworkcontext +pnetworkcontext posix pparsedresponse ppm @@ -60,21 +82,32 @@ prequesttime prequesttxtime presponsebuffer presponsecode +presponsedata presponsepacket presponserxtime +pservername pserverrxtime +pservertime pservertxtime psntptime +ptimeserver +ptimeservers ptr +pudptransportintf punixtimemicrosecs punixtimesecs +pusercontext pwordmemory randomnum randomnumber receivetime +recv +recvfrom refid reftime rejectedresponsecode +resolvednsfunc +responsesize retryable rfc rootdelay @@ -84,10 +117,13 @@ rstr rx secsinnetorder secsinnetorder +sendto serializerequest +setsystemtimefunc sntp sntpbuffertoosmall sntpclockoffsetoverflow +sntperrorauthfailure sntperrorbadparameter sntperrorbuffertoosmall sntperrortimenotsupported @@ -95,6 +131,7 @@ sntpinvalidresponse sntprejectedresponsechangeserver sntprejectedresponseothercode sntprejectedresponseretrywithbackoff +sntpservernotauthenticated sntpsuccess sntptimestamp sntpv @@ -106,6 +143,7 @@ sublicense transmittime trng tx +udp uint unix utc diff --git a/source/core_sntp_client.c b/source/core_sntp_client.c new file mode 100644 index 0000000..a255f37 --- /dev/null +++ b/source/core_sntp_client.c @@ -0,0 +1,104 @@ +/* + * 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_client.c + * @brief Implementation of the client API of the coreSNTP library. + */ + +/* Standard includes. */ +#include +#include + +/* SNTP client library API include. */ +#include "core_sntp_client.h" + + +SntpStatus_t Sntp_Init( SntpContext_t * pContext, + const SntpServerInfo_t * pTimeServers, + size_t numOfServers, + uint8_t * pNetworkBuffer, + size_t bufferSize, + SntpResolveDns_t resolveDnsFunc, + SntpGetTime_t getSystemTimeFunc, + SntpSetTime_t setSystemTimeFunc, + const UdpTransportInterface_t * pTransportIntf, + const SntpAuthenticationInterface_t * pAuthIntf ) +{ + SntpStatus_t status = SntpSuccess; + + /* Validate pointer parameters are not NULL. */ + if( ( pContext == NULL ) || ( pTimeServers == NULL ) || ( numOfServers == 0U ) || + ( pNetworkBuffer == NULL ) || ( resolveDnsFunc == NULL ) || ( getSystemTimeFunc == NULL ) || + ( setSystemTimeFunc == NULL ) || ( pTransportIntf == NULL ) ) + { + status = SntpErrorBadParameter; + } + /* Validate that the members of the UDP transport interface. */ + else if( ( pTransportIntf->recvFrom == NULL ) || ( pTransportIntf->sendTo == NULL ) ) + { + status = SntpErrorBadParameter; + } + + /* If an authentication interface is provided, validate that its function pointer + * members are valid. */ + else if( ( pAuthIntf != NULL ) && + ( ( pAuthIntf->generateClientAuth == NULL ) || + ( pAuthIntf->validateServer == NULL ) ) ) + { + status = SntpErrorBadParameter; + } + else if( bufferSize < SNTP_PACKET_BASE_SIZE ) + { + status = SntpErrorBufferTooSmall; + } + else + { + /* Reset the context memory to zero. */ + ( void ) memset( pContext, 0, sizeof( SntpContext_t ) ); + + /* Set the members of the context with passed parameters. */ + pContext->pTimeServers = pTimeServers; + pContext->numOfServers = numOfServers; + + pContext->pNetworkBuffer = pNetworkBuffer; + pContext->bufferSize = bufferSize; + + pContext->resolveDnsFunc = resolveDnsFunc; + pContext->getTimeFunc = getSystemTimeFunc; + pContext->setTimeFunc = setSystemTimeFunc; + + /* Copy contents of UDP transport interface to context. */ + ( void ) memcpy( &pContext->networkIntf, pTransportIntf, sizeof( UdpTransportInterface_t ) ); + + /* If authentication interface has been passed, copy its contents to the context. */ + if( pAuthIntf != NULL ) + { + ( void ) memcpy( &pContext->authIntf, pAuthIntf, sizeof( SntpAuthenticationInterface_t ) ); + } + + /* Initialize the packet size member to the standard minimum SNTP packet size.*/ + pContext->sntpPacketSize = SNTP_PACKET_BASE_SIZE; + } + + return status; +} diff --git a/source/include/core_sntp_client.h b/source/include/core_sntp_client.h new file mode 100644 index 0000000..c527ba7 --- /dev/null +++ b/source/include/core_sntp_client.h @@ -0,0 +1,474 @@ +/* + * 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_client.h + * @brief API of an SNTPv4 client library that can send time requests and receive time response to/from + * SNTP/NTP servers. The library follows the Best Practices suggested in the the SNTPv4 specification, + * [RFC 4330](https://tools.ietf.org/html/rfc4330). + * The library can be used to run an SNTP client in a dedicated deamon task to periodically synchronize + * time from the Internet. + */ + +#ifndef CORE_SNTP_CLIENT_H_ +#define CORE_SNTP_CLIENT_H_ + +/* Standard include. */ +#include +#include +#include + +/* Include coreSNTP Serializer header. */ +#include "core_sntp_serializer.h" + +/** + * @ingroup core_sntp_callback_types + * @brief Interface for user-defined function to resolve time server domain-name + * to an IPv4 address. + * The SNTP client library attempts to resolve the DNS of the time-server being + * used every time the @ref Sntp_SendTimeRequest API is called. + * + * @param[in] pTimeServer The time-server whose IPv4 address is to be resolved. + * @param[out] pIpV4Addr This should be filled with the resolved IPv4 address. + * of @p pTimeServer. + * + * @return `true` if DNS resolution is successful; otherwise `false` to represent + * failure. + */ +typedef bool ( * SntpResolveDns_t )( const char * pServerAddr, + uint32_t * pIpV4Addr ); + +/** + * @ingroup core_sntp_callback_types + * @brief Interface for user-defined function to obtain the current system time + * in SNTP timestamp format. + * + * @note If your platform follows UNIX representation of time, the + * #SNTP_TIME_AT_UNIX_EPOCH_SECS and #SNTP_FRACTION_VALUE_PER_MICROSECOND macros + * can be used to convert UNIX time to SNTP timestamp. + * + * @param[out] pCurrentTime This should be filled with the current system time + * in SNTP timestamp format. + * + * @return `true` if obtaining system time is successful; otherwise `false` to + * represent failure. + */ +typedef bool ( * SntpGetTime_t )( SntpTimestamp_t * pCurrentTime ); + +/** + * @ingroup core_sntp_callback_types + * @brief Interface for user-defined function to update the system clock time + * so that it is synchronized the time server used for getting current time. + * + * @param[in] pTimeServer The time server used to request time. + * @param[in] pServerTime The current time returned by the @p pTimeServer. + * @param[in] clockOffSetSec The calculated clock offset of the system relative + * to the server time. + * + * @note The user can use either a "step" or "slew" clock discipline methodology + * depending on the application needs. + * If the application requires a smooth time continuum of system time is required, + * then the "slew" discipline methodology can be used with the clock offset value, + * @p clockOffSetSec, to apply correction to the system clock with a "slew rate" + * (that is higher than the SNTP polling rate). + * If the application can accept sudden jump in time (forward or backward), then + * the "step" discipline methodology can be used to directly update the system + * clock with the current server time, @p pServerTime, every time the coreSNTP + * library calls the interface. + * + * @return `true` if setting system time is successful; otherwise `false` to + * represent failure. + */ +typedef bool ( * SntpSetTime_t )( const char * pTimeServer, + const SntpTimestamp_t * pServerTime, + int32_t clockOffsetSec ); + +/** + * @brief The default UDP port supported by SNTP/NTP servers for client-server + * communication. + * + * @note It is possible for a server to use a different port number than + * the default port when using the Network Time Security protocol as the security + * mechanism for SNTP communication. For more information, refer to Section 4.1.8 + * of [RFC 8915](https://tools.ietf.org/html/rfc8915). + */ +#define SNTP_DEFAULT_SERVER_PORT ( 123U ) + +/** + * @brief core_sntp_struct_types + * @brief Structure representing information for a time server. + */ +typedef struct SntpServerInfo +{ + const char * pServerName; /**<@brief The time server endpoint. */ + uint16_t port; /**<@brief The UDP port supported by the server + * for SNTP/NTP communication. */ +} SntpServerInfo_t; + +/** + * @ingroup core_sntp_struct_types + * @typedef NetworkContext_t + * @brief A user-defined type for context that is passed to the transport interface functions. + * It MUST be defined by the user to use the library. + * It is of incomplete type to allow user to define to the needs of their transport + * interface implementation. + */ +struct NetworkContext; +typedef struct NetworkContext NetworkContext_t; + +/** + * @ingroup core_sntp_callback_types + * @brief Interface for user-defined function to send data to the network + * over User Datagram Protocol (UDP). + * + * @param[in,out] pNetworkContext The user defined NetworkContext_t which + * is opaque to the coreSNTP library. + * @param[in] pTimeServer The time server to send the data to. + * @param[in] pBuffer The buffer containing the data to send over the network. + * @param[in] bytesToSend The size of data in @p pBuffer to send. + * + * @return The function SHOULD return one of the following integer codes: + * - @p bytesToSend when all requested data is successfully transmitted over the + * network. + * - >0 value representing number of bytes sent when only partial data is sent + * over the network. + * - 0 when no data could be sent over the network (due to network buffer being + * full, for example), and the send operation can be retried. + * - -2 when the send operation failed to send any data due to an internal error, + * and operation cannot be retried. + */ +typedef int32_t ( * UdpTransportSendTo_t )( NetworkContext_t * pNetworkContext, + const SntpServerInfo_t * pTimeServer, + const void * pBuffer, + size_t bytesToSend ); + +/** + * @ingroup core_sntp_callback_types + * @brief Interface for user-defined function to receive data from the network + * over User Datagram Protocol (UDP). + * + * @param[in,out] pNetworkContext The user defined NetworkContext_t which + * is opaque to the coreSNTP library. + * @param[in] pTimeServer The time server to receive data from. + * @param[out] pBuffer This SHOULD be filled with data received from the network. + * @param[in] bytesToRecv The expected number of bytes to receive from the + * server. + * + * @return The function SHOULD return one of the following integer codes: + * - @p bytesToRecv value if all the requested number of bytes are received + * from the network. + * - > 0 value representing number of bytes received when partial data is + * received from the network. + * - ZERO when no data is available on the network, and the operation can be + * retried. + * - -2 when the read operation failed due to internal error, and operation cannot + * be retried. + */ +typedef int32_t ( * UdpTransportRecvFrom_t )( NetworkContext_t * pNetworkContext, + SntpServerInfo_t * pTimeServer, + void * pBuffer, + size_t bytesToRecv ); + +/** + * @ingroup core_sntp_struct_types + * @brief Struct representing the UDP transport interface for user-defined functions + * that coreSNTP library depends on for performing read/write network operations. + */ +typedef struct UdpTransportIntf +{ + NetworkContext_t * pUserContext; /**<@brief The user-defined context for storing + * network socket information. */ + UdpTransportSendTo_t sendTo; /**<@brief The user-defined UDP send function. */ + UdpTransportRecvFrom_t recvFrom; /**<@brief The user-defined UDP receive function. */ +} UdpTransportInterface_t; + +/** + * @ingroup core_sntp_struct_types + * @typedef SntpAuthContext_t + * @brief A user-defined type for context that is passed to the authentication interface functions. + * It MUST be defined by the user to use the library. + * It is of incomplete type to allow user to defined to the the needs of their authentication + * interface implementation. + */ +struct SntpAuthContext; +typedef struct SntpAuthContext SntpAuthContext_t; + +/** + * @ingroup core_sntp_callback_types + * @brief Interface for user-defined function to generate and append + * authentication code in an SNTP request buffer for the SNTP client to be + * authenticated by the time server, if a security mechanism is used. + * + * The user can choose to implement with any security mechanism, symmetric + * key-based (like AES-CMAC) or asymmetric key-based (like Network Time Security), + * depending on the security mechanism supported by the time server being used + * to synchronize time with. + * + * @note The function SHOULD generate the authentication data for the first + * #SNTP_PACKET_BASE_SIZE bytes of SNTP request packet present in the passed buffer + * @p pBuffer, and fill the generated authentication data after #SNTP_PACKET_BASE_SIZE + * bytes in the buffer. + * + * @param[in,out] pContext The user defined NetworkContext_t which + * is opaque to the coreSNTP library. + * @param[in] pTimeServer The time server being used to request time from. + * This parameter is useful to choose the security mechanism when multiple time + * servers are configured in the library, and they require different security + * mechanisms or authentication credentials to use. + * @param[in, out] pBuffer This buffer SHOULD be filled with the authentication + * code generated from the #SNTP_PACKET_BASE_SIZE bytes of SNTP request data + * present in it. + * @param[in] bufferSize The maximum amount of data that can be held by + * the buffer, @p pBuffer. + * @param[out] pAuthCodeSize The size of authentication data filled in the buffer. + * + * @return The function SHOULD return one of the following integer codes: + * - #SntpSuccess when the server is successfully authenticated. + * - #SntpErrorBufferTooSmall when the user-supplied buffer (to the SntpContext_t through + * Sntp_Init) is not large enough to hold authentication data. + * - #SntpErrorAuthFailure for failure to generate authentication data due to internal + * error. + */ +typedef SntpStatus_t (* SntpGenerateAuthCode_t )( SntpAuthContext_t * pContext, + const char * pTimeServer, + void * pBuffer, + size_t bufferSize, + size_t * pAuthCodeSize ); + +/** + * @ingroup core_sntp_callback_types + * @brief Interface for user-defined function to authenticate server by validating + * the authentication code present in its SNTP response to a time request, if + * a security mechanism is supported by the server. + * + * The user can choose to implement with any security mechanism, symmetric + * key-based (like AES-CMAC) or asymmetric key-based (like Network Time Security), + * depending on the security mechanism supported by the time server being used + * to synchronize time with. + * + * @note In an SNTP response, the authentication code is present only after the + * first #SNTP_PACKET_BASE_SIZE bytes. Depending on the security mechanism used, + * the first #SNTP_PACKET_BASE_SIZE bytes MAY be used in validating the + * authentication data sent by the server. + * + * @param[in,out] pContext The user defined NetworkContext_t which + * is opaque to the coreSNTP library. + * @param[in] pTimeServer The time server that has to be authenticated from its + * SNTP response. + * This parameter is useful to choose the security mechanism when multiple time + * servers are configured in the library, and they require different security + * mechanisms or authentication credentials to use. + * @param[in] pResponseData The SNTP response from the server that contains the + * authentication code after the first #SNTP_PACKET_BASE_SIZE bytes. + * @param[in] responseSize The total size of the response from the server. + * + * @return The function SHOULD return one of the following integer codes: + * - #SntpSuccess when the server is successfully authenticated. + * - #SntpServerNotAuthenticated when server could not be authenticated. + * - #SntpErrorAuthFailure for failure to authenticate server due to internal + * error. + */ +typedef SntpStatus_t (* SntpValidateAuthCode_t )( SntpAuthContext_t * pContext, + const char * pTimeServer, + const void * pResponseData, + size_t responseSize ); + +/** + * @ingroup core_sntp_struct_types + * @brief Struct representing the authentication interface for securely + * communicating with time servers. + * + * @note Using a security mechanism is OPTIONAL for using the coreSNTP + * library i.e. a user does not need to define the authentication interface + * if they are not using a security mechanism for SNTP communication. + */ +typedef struct SntpAuthenticationIntf +{ + /** + *@brief The user-defined context for storing information like + * key credentials required for cryptographic operations in the + * security mechanism used for communicating with server. + */ + SntpAuthContext_t * pAuthContext; + + /** + * @brief The user-defined function for appending client authentication data. + * */ + SntpGenerateAuthCode_t generateClientAuth; + + /** + * @brief The user-defined function to authenticating server from its SNTP + * response. + */ + SntpValidateAuthCode_t validateServer; +} SntpAuthenticationInterface_t; + +/** + * @ingroup core_sntp_struct_types + * @brief Structure for a context that stores state for managing a long-running + * SNTP client that periodically polls time and synchronizes system clock. + */ +typedef struct SntpContext +{ + /** + * @brief List of time servers in decreasing priority order configured + * for the SNTP client. + * Only a single server is configured for use at a time across polling + * attempts until the server rejects a time request or there is a response + * timeout, after which, the next server in the list is used for subsequent + * polling requests. + */ + const SntpServerInfo_t * pTimeServers; + + /** + * @brief Number of servers configured for use. + */ + size_t numOfServers; + + /** + * @brief The index for the currently configured time server for time querying + * from the list of time servers in @ref pTimeServers. + */ + size_t currentServerIndex; + + /** + * @brief The user-supplied buffer for storing network data of both SNTP requests + * and SNTP response. + */ + uint8_t * pNetworkBuffer; + + /** + * @brief The size of the network buffer. + */ + size_t bufferSize; + + /** + * @brief The user-supplied function for resolving DNS name of time servers. + */ + SntpResolveDns_t resolveDnsFunc; + + /** + * @brief The user-supplied function for obtaining the current system time. + */ + SntpGetTime_t getTimeFunc; + + /** + * @brief The user-supplied function for correcting system time after receiving + * time from a server. + */ + SntpSetTime_t setTimeFunc; + + /** + * @brief The user-defined interface for performing User Datagram Protocol (UDP) + * send and receive network operations. + */ + UdpTransportInterface_t networkIntf; + + /** + * @brief The user-defined interface for incorporating security mechanism of + * adding client authentication in SNTP request as well as authenticating server + * from SNTP response. + * + * @note If the application will not use security mechanism for any of the + * configured servers, then this interface can be undefined. + */ + SntpAuthenticationInterface_t authIntf; + + /** + * @brief Cache of the resolved Ipv4 address of the current server being used for + * time synchronization. + * As a Best Practice functionality, the client library attempts to resolve the + * DNS of the time-server every time the @ref Sntp_SendTimeRequest API is called. + */ + uint32_t currentServerIpV4Addr; + + /** + * @brief Cache of the timestamp of sending the last time request to a server + * for replay attack protection by checking that the server response contains + * the same timestamp in its "originate timestamp" field. + */ + SntpTimestamp_t lastRequestTime; + + /** + * @brief State variable for storing the size of the SNTP packet that includes + * both #SNTP_PACKET_BASE_SIZE bytes plus any authentication data, if a security + * mechanism is used. + * This state variable is used for expecting the same size for an SNTP response + * from the server. + */ + size_t sntpPacketSize; +} SntpContext_t; + +/** + * @brief Initializes a context for SNTP client communication with SNTP/NTP + * servers. + * + * @param[out] pContext The user-supplied memory for the context that will be + * initialized to represent an SNTP client. + * @param[in] pTimeServers The list of decreasing order of priority of time + * servers that should be used by the SNTP client. This list MUST stay in + * scope for all the time of use of the context. + * @param[in] numOfServers The number of servers in the list, @p pTimeServers. + * @param[in] pNetworkBuffer The user-supplied memory that will be used for + * storing network data for SNTP client-server communication. The buffer + * MUST stay in scope for all the time of use of the context. + * @param[in] bufferSize The size of the passed buffer @p pNetworkBuffer. The buffer + * SHOULD be appropriately sized for storing an entire SNTP packet which includes + * both #SNTP_PACKET_BASE_SIZE bytes of standard SNTP packet size, and space for + * authentication data, if security mechanism is used to communicate with any of + * the time servers configured for use. + * @param[in] resolveDnsFunc The user-defined function for DNS resolution of time + * server. + * @param[in] getSystemTimeFunc The user-defined function for querying system + * time. + * @param[in] setSystemTimeFunc The user-defined function for correcting system + * time for every successful time response received from a server. + * @param[in] pUdpTransportIntf The user-defined function for performing network + * send/recv operations over UDP. + * @param[in] pAuthIntf The user-defined interface for generating client authentication + * in SNTP requests and authenticating servers in SNTP responses, if security mechanism + * is used in SNTP communication with server(s). If security mechanism is not used in + * communication with any of the configured servers (in @p pTimeServers), then the + * @ref SntpAuthenticationInterface_t does not need to be defined and this parameter + * can be NULL. + * + * @return This function returns one of the following: + * - #SntpSuccess if the context is initialized. + * - #SntpErrorBadParameter if any of the passed parameters in invalid. + * - #SntpErrorBufferTooSmall if the buffer does not have the minimum size + * required for a valid SNTP response packet. + */ +/* @[define_sntp_init] */ +SntpStatus_t Sntp_Init( SntpContext_t * pContext, + const SntpServerInfo_t * pTimeServers, + size_t numOfServers, + uint8_t * pNetworkBuffer, + size_t bufferSize, + SntpResolveDns_t resolveDnsFunc, + SntpGetTime_t getSystemTimeFunc, + SntpSetTime_t setSystemTimeFunc, + const UdpTransportInterface_t * pTransportIntf, + const SntpAuthenticationInterface_t * pAuthIntf ); +/* @[define_sntp_init] */ + + +#endif /* ifndef CORE_SNTP_CLIENT_H_ */ diff --git a/source/include/core_sntp_serializer.h b/source/include/core_sntp_serializer.h index a3293e5..0d1d770 100644 --- a/source/include/core_sntp_serializer.h +++ b/source/include/core_sntp_serializer.h @@ -135,7 +135,6 @@ */ #define SNTP_CLOCK_OFFSET_OVERFLOW ( 0x7FFFFFFF ) - /** * @ingroup core_sntp_enum_types * @brief Enumeration of status codes that can be returned @@ -198,7 +197,21 @@ typedef enum SntpStatus * @brief SNTP timestamp cannot be converted to UNIX time as time does not lie * in time range supported by Sntp_ConvertToUnixTime. */ - SntpErrorTimeNotSupported + SntpErrorTimeNotSupported, + + /** + * @brief Time server is not authenticated from the authentication data in its response. + * This status can be returned by the user-supplied definition of the + * @ref SntpValidateAuthCode_t authentication interface. + */ + SntpServerNotAuthenticated, + + /** + * @brief Failure from the user-supplied authentication interface, @ref SntpAuthenticationIntf_t, + * in either generating authentication data for SNTP request OR validating the authentication + * data in SNTP response from server. + */ + SntpErrorAuthFailure } SntpStatus_t; /** @@ -225,9 +238,12 @@ typedef enum SntpLeapSecondInfo /** * @ingroup core_sntp_struct_types * @brief Structure representing an SNTP timestamp. + * * @note The SNTP timestamp uses 1st January 1900 0h 0m 0s Coordinated Universal Time (UTC) * as the primary epoch i.e. the timestamp represents current time as the amount of time since * the epoch time. + * Refer to the [SNTPv4 specification](https://tools.ietf.org/html/rfc4330#section-3) for more + * information of the SNTP timestamp format. */ typedef struct SntpTimestamp { @@ -273,6 +289,10 @@ typedef struct SntpResponse * times. This information can be used to synchronize the system clock * with a "slew" or "step" correction approach. * + * @note The library calculates the clock-offset value using the On-Wire + * protocol suggested by the NTPv4 specification. For more information, + * refer to https://tools.ietf.org/html/rfc5905#section-8. + * * @note The system clock MUST be within 34 years (in the past or future) * of the server time for this calculation. This is a fundamental limitation * of 64 bit integer arithmetic. diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index fd8864a..6aca07b 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -82,6 +82,6 @@ add_subdirectory( unit-test ) add_custom_target( coverage COMMAND ${CMAKE_COMMAND} -DUNITY_DIR=${UNITY_DIR} -P ${MODULE_ROOT_DIR}/tools/unity/coverage.cmake - DEPENDS unity core_sntp_utest + DEPENDS unity core_sntp_client_utest core_sntp_serializer_utest WORKING_DIRECTORY ${CMAKE_BINARY_DIR} ) diff --git a/test/unit-test/CMakeLists.txt b/test/unit-test/CMakeLists.txt index 5460d00..f1ceb6f 100644 --- a/test/unit-test/CMakeLists.txt +++ b/test/unit-test/CMakeLists.txt @@ -61,7 +61,7 @@ list(APPEND utest_dep_list ${real_name} ) -set(utest_name "${project_name}_utest") +set(utest_name "${project_name}_serializer_utest") set(utest_source "${project_name}_serializer_utest.c") create_test(${utest_name} ${utest_source} @@ -69,3 +69,12 @@ create_test(${utest_name} "${utest_dep_list}" "${test_include_directories}" ) + +set(utest_name "${project_name}_client_utest") +set(utest_source "${project_name}_client_utest.c") +create_test(${utest_name} + ${utest_source} + "${utest_link_list}" + "${utest_dep_list}" + "${test_include_directories}" + ) diff --git a/test/unit-test/core_sntp_client_utest.c b/test/unit-test/core_sntp_client_utest.c new file mode 100644 index 0000000..9457a37 --- /dev/null +++ b/test/unit-test/core_sntp_client_utest.c @@ -0,0 +1,438 @@ +/* + * 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. + */ + +/* Standard includes. */ +#include +#include +#include +#include + +/* POSIX include. */ +#include + +/* Unity include. */ +#include "unity.h" + +/* coreSNTP Client API include */ +#include "core_sntp_client.h" + +/* Test IPv4 address for time server. */ +#define TEST_SERVER_ADDR ( 0xAABBCCDD ) + +typedef struct NetworkContext +{ + int udpSocket; +} NetworkContext_t; + +typedef struct SntpAuthContext +{ + uint32_t keyId; +} SntpAuthContext_t; + +/* Global variables common to test cases. */ +static SntpContext_t context; +static uint8_t testBuffer[ 100 ]; +static SntpServerInfo_t testServers[] = +{ + { + "my.ntp.server.1", + SNTP_DEFAULT_SERVER_PORT + }, + { + "my.ntp.server.2", + SNTP_DEFAULT_SERVER_PORT + } +}; +static UdpTransportInterface_t transportIntf; +static NetworkContext_t netContext; +static SntpAuthenticationInterface_t authIntf; +static SntpAuthContext_t authContext; + +/* Variables for configuring behavior of interface functions. */ +static bool dnsResolveRetCode = true; +static uint32_t dnsResolveAddr = TEST_SERVER_ADDR; +static bool getTimeRetCode = true; +static bool setTimeRetCode = true; +static int32_t UpdSendRetCode = 0; +static int32_t UpdRecvCode = 0; + +/* ========================= Helper Functions ============================ */ + +/* Test definition of the @ref SntpResolveDns_t interface. */ +bool dnsResolve( const char * pServerAddr, + uint32_t * pIpV4Addr ) +{ + TEST_ASSERT_NOT_NULL( pServerAddr ); + TEST_ASSERT_NOT_NULL( pIpV4Addr ); + + *pIpV4Addr = TEST_SERVER_ADDR; + + return dnsResolveRetCode; +} + +/* Test definition of the @ref SntpGetTime_t interface. */ +bool getTime( SntpTimestamp_t * pCurrentTime ) +{ + TEST_ASSERT_NOT_NULL( pCurrentTime ); + + return getTimeRetCode; +} + +/* Test definition of the @ref SntpSetTime_t interface. */ +bool setTime( const char * pTimeServer, + const SntpTimestamp_t * pServerTime, + int32_t clockOffsetSec ) +{ + TEST_ASSERT_NOT_NULL( pTimeServer ); + TEST_ASSERT_NOT_NULL( pServerTime ); + ( void ) clockOffsetSec; + + return setTimeRetCode; +} + +/* Test definition of the @ref UdpTransportSendTo_t interface. */ +int32_t UdpSendTo( NetworkContext_t * pNetworkContext, + const SntpServerInfo_t * pTimeServer, + const void * pBuffer, + size_t bytesToSend ) +{ + TEST_ASSERT_NOT_NULL( pNetworkContext ); + TEST_ASSERT_NOT_NULL( pTimeServer ); + TEST_ASSERT_NOT_NULL( pBuffer ); + TEST_ASSERT_GREATER_OR_EQUAL( SNTP_PACKET_BASE_SIZE, bytesToSend ); + + return UpdSendRetCode; +} + +/* Test definition of the @ref UdpTransportRecvFrom_t interface. */ +int32_t UdpRecvFrom( NetworkContext_t * pNetworkContext, + SntpServerInfo_t * pTimeServer, + void * pBuffer, + size_t bytesToRecv ) +{ + TEST_ASSERT_NOT_NULL( pNetworkContext ); + TEST_ASSERT_NOT_NULL( pTimeServer ); + TEST_ASSERT_NOT_NULL( pBuffer ); + TEST_ASSERT_GREATER_OR_EQUAL( SNTP_PACKET_BASE_SIZE, bytesToRecv ); + + return UpdRecvCode; +} + +/* Test definition for @ref SntpGenerateAuthCode_t interface. */ +SntpStatus_t generateClientAuth( SntpAuthContext_t * pContext, + const char * pTimeServer, + void * pBuffer, + size_t bufferSize, + size_t * pAuthCodeSize ) +{ + TEST_ASSERT_NOT_NULL( pContext ); + TEST_ASSERT_NOT_NULL( pTimeServer ); + TEST_ASSERT_NOT_NULL( pBuffer ); + TEST_ASSERT_NOT_NULL( pAuthCodeSize ); + TEST_ASSERT_GREATER_OR_EQUAL( SNTP_PACKET_BASE_SIZE, bufferSize ); + + return SntpSuccess; +} + +/* Test definition for @ref SntpValidateAuthCode_t interface. */ +SntpStatus_t validateServer( SntpAuthContext_t * pContext, + const char * pTimeServer, + const void * pResponseData, + size_t responseSize ) +{ + TEST_ASSERT_NOT_NULL( pContext ); + TEST_ASSERT_NOT_NULL( pTimeServer ); + TEST_ASSERT_NOT_NULL( pResponseData ); + TEST_ASSERT_GREATER_OR_EQUAL( SNTP_PACKET_BASE_SIZE, responseSize ); + + return SntpSuccess; +} + +/* ============================ UNITY FIXTURES ============================ */ + +/* Called before each test method. */ +void setUp() +{ + /* Reset the global variables. */ + dnsResolveRetCode = true; + dnsResolveAddr = TEST_SERVER_ADDR; + getTimeRetCode = true; + setTimeRetCode = true; + UpdSendRetCode = 0; + UpdRecvCode = 0; + + /* Set the transport interface object. */ + transportIntf.pUserContext = &netContext; + transportIntf.sendTo = UdpSendTo; + transportIntf.recvFrom = UdpRecvFrom; + + /* Set the auth interface object. */ + authIntf.pAuthContext = &authContext; + authIntf.generateClientAuth = generateClientAuth; + authIntf.validateServer = validateServer; + + /* Clear the network buffer. */ + memset( &testBuffer, 0, sizeof( testBuffer ) ); +} + +/* Called at the beginning of the whole suite. */ +void suiteSetUp() +{ +} + +/* Called at the end of the whole suite. */ +int suiteTearDown( int numFailures ) +{ + return numFailures; +} + +/* ========================================================================== */ + +/** + * @brief Test @ref Sntp_Init with invalid parameters. + */ +void test_Init_InvalidParams( void ) +{ + /* Pass invalid context memory. */ + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( NULL, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + dnsResolve, + getTime, + setTime, + &transportIntf, + NULL ) ); + + /* Pass invalid list of time servers. */ + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + NULL, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + dnsResolve, + getTime, + setTime, + &transportIntf, + NULL ) ); + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + 0, + testBuffer, + sizeof( testBuffer ), + dnsResolve, + getTime, + setTime, + &transportIntf, + NULL ) ); + + /* Pass invalid network buffer. */ + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + NULL, + sizeof( testBuffer ), + dnsResolve, + getTime, + setTime, + &transportIntf, + NULL ) ); + TEST_ASSERT_EQUAL( SntpErrorBufferTooSmall, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + SNTP_PACKET_BASE_SIZE / 2, + dnsResolve, + getTime, + setTime, + &transportIntf, + NULL ) ); + + /* Pass invalid required interface definitions. */ + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + NULL, + getTime, + setTime, + &transportIntf, + NULL ) ); + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + dnsResolve, + NULL, + setTime, + &transportIntf, + NULL ) ); + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + dnsResolve, + getTime, + NULL, + &transportIntf, + NULL ) ); + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + dnsResolve, + getTime, + setTime, + NULL, + NULL ) ); + + /* Pass valid transport interface object but invalid members. */ + transportIntf.recvFrom = NULL; + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + dnsResolve, + getTime, + setTime, + &transportIntf, + NULL ) ); + transportIntf.recvFrom = UdpRecvFrom; + transportIntf.sendTo = NULL; + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + dnsResolve, + getTime, + setTime, + &transportIntf, + NULL ) ); + + /* Set the transport interface object to be valid for next test. */ + transportIntf.sendTo = UdpSendTo; + + /* Pass valid authentication interface object but invalid members. */ + authIntf.generateClientAuth = NULL; + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + dnsResolve, + getTime, + setTime, + &transportIntf, + &authIntf ) ); + authIntf.generateClientAuth = generateClientAuth; + authIntf.validateServer = NULL; + TEST_ASSERT_EQUAL( SntpErrorBadParameter, + Sntp_Init( &context, + testServers, + sizeof( testServers ) / sizeof( SntpServerInfo_t ), + testBuffer, + sizeof( testBuffer ), + dnsResolve, + getTime, + setTime, + &transportIntf, + &authIntf ) ); +} + +/** + * @brief Test @ref Sntp_Init API correctly initializes a context. + */ +void test_Init_Nominal( void ) +{ +#define TEST_SNTP_INIT_SUCCESS( pAuthIntf ) \ + do { \ + /* Call the API under test. */ \ + TEST_ASSERT_EQUAL( SntpSuccess, \ + Sntp_Init( &context, \ + testServers, \ + sizeof( testServers ) / sizeof( SntpServerInfo_t ), \ + testBuffer, \ + sizeof( testBuffer ), \ + dnsResolve, \ + getTime, \ + setTime, \ + &transportIntf, \ + pAuthIntf ) ); \ + \ + /* Make sure that the passed parameters have been set in the context. */ \ + TEST_ASSERT_EQUAL( testServers, context.pTimeServers ); \ + TEST_ASSERT_EQUAL( sizeof( testServers ) / sizeof( SntpServerInfo_t ), context.numOfServers ); \ + TEST_ASSERT_EQUAL_PTR( testBuffer, context.pNetworkBuffer ); \ + TEST_ASSERT_EQUAL( sizeof( testBuffer ), context.bufferSize ); \ + TEST_ASSERT_EQUAL_PTR( dnsResolve, context.resolveDnsFunc ); \ + TEST_ASSERT_EQUAL_PTR( getTime, context.getTimeFunc ); \ + TEST_ASSERT_EQUAL_PTR( setTime, context.setTimeFunc ); \ + TEST_ASSERT_EQUAL_MEMORY( &transportIntf, \ + &context.networkIntf, \ + sizeof( UdpTransportInterface_t ) ); \ + if( pAuthIntf == NULL ) \ + { \ + TEST_ASSERT_NULL( context.authIntf.pAuthContext ); \ + TEST_ASSERT_NULL( context.authIntf.generateClientAuth ); \ + TEST_ASSERT_NULL( context.authIntf.validateServer ); \ + } \ + else \ + { \ + TEST_ASSERT_EQUAL_MEMORY( &authIntf, &context.authIntf, sizeof( SntpAuthenticationInterface_t ) ); \ + } \ + \ + /* Validate the initialization of the state members of the context. */ \ + TEST_ASSERT_EQUAL( 0, context.currentServerIndex ); \ + TEST_ASSERT_EQUAL( 0, context.currentServerIpV4Addr ); \ + TEST_ASSERT_EQUAL( 0, context.lastRequestTime.seconds ); \ + TEST_ASSERT_EQUAL( 0, context.lastRequestTime.fractions ); \ + TEST_ASSERT_EQUAL( SNTP_PACKET_BASE_SIZE, context.sntpPacketSize ); \ + } while( 0 ) + + /* Test when an authentication interface is not passed. */ + TEST_SNTP_INIT_SUCCESS( NULL ); + + /* Reset the context memory. */ + memset( &context, 0, sizeof( SntpContext_t ) ); + + /* Test with a valid authentication interface. */ + TEST_SNTP_INIT_SUCCESS( &authIntf ); +} From 6a88aca5e0ffb567576e02af47acc6879a9a89f8 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Mon, 3 May 2021 17:26:32 -0700 Subject: [PATCH 04/44] Revert "Set up litani infra for coreSNTP" This reverts commit 6f2017e9deeb3becd714ba1ba1a1596f180055ad. --- test/cbmc/.gitignore | 23 -- test/cbmc/include/README.md | 1 - test/cbmc/negative_tests/README.md | 1 - test/cbmc/negative_tests/assert/Makefile | 1 - .../negative_tests/assert/assert_harness.c | 1 - .../cbmc/negative_tests/bounds_check/Makefile | 1 - .../bounds_check/bounds_check_harness.c | 1 - .../negative_tests/conversion_check/Makefile | 1 - .../conversion_check_harness.c | 1 - .../negative_tests/div_by_zero_check/Makefile | 1 - .../div_by_zero_check_harness.c | 1 - .../float_overflow_check/Makefile | 1 - .../float_overflow_check_harness.c | 1 - .../float_underflow_check/Makefile | 1 - .../float_underflow_check_harness.c | 1 - test/cbmc/negative_tests/nan_check/Makefile | 1 - .../nan_check/nan_check_harness.c | 1 - .../negative_tests/pointer_check/Makefile | 1 - .../pointer_check/pointer_check_harness.c | 1 - .../pointer_overflow_check/Makefile | 1 - .../pointer_overflow_check_harness.c | 1 - .../pointer_primitive_check/Makefile | 1 - .../pointer_primitive_check_harness.c | 1 - .../pointer_underflow_check/Makefile | 1 - .../pointer_underflow_check_harness.c | 1 - .../signed_overflow_check/Makefile | 1 - .../signed_overflow_check_harness.c | 1 - .../signed_underflow_check/Makefile | 1 - .../signed_underflow_check_harness.c | 1 - .../undefined_shift_check/Makefile | 1 - .../undefined_shift_check_harness.c | 1 - .../unsigned_overflow_check/Makefile | 1 - .../unsigned_overflow_check_harness.c | 1 - .../unsigned_underflow_check/Makefile | 1 - .../unsigned_underflow_check_harness.c | 1 - test/cbmc/proofs/Makefile-project-defines | 37 --- test/cbmc/proofs/Makefile-project-targets | 10 - test/cbmc/proofs/Makefile-project-testing | 11 - test/cbmc/proofs/Makefile-template-defines | 19 -- test/cbmc/proofs/Makefile.common | 1 - test/cbmc/proofs/README.md | 1 - test/cbmc/proofs/prepare.py | 1 - test/cbmc/proofs/run-cbmc-proofs.py | 259 ------------------ test/cbmc/sources/README.md | 1 - test/cbmc/stubs/README.md | 1 - 45 files changed, 398 deletions(-) delete mode 100644 test/cbmc/.gitignore delete mode 120000 test/cbmc/include/README.md delete mode 120000 test/cbmc/negative_tests/README.md delete mode 120000 test/cbmc/negative_tests/assert/Makefile delete mode 120000 test/cbmc/negative_tests/assert/assert_harness.c delete mode 120000 test/cbmc/negative_tests/bounds_check/Makefile delete mode 120000 test/cbmc/negative_tests/bounds_check/bounds_check_harness.c delete mode 120000 test/cbmc/negative_tests/conversion_check/Makefile delete mode 120000 test/cbmc/negative_tests/conversion_check/conversion_check_harness.c delete mode 120000 test/cbmc/negative_tests/div_by_zero_check/Makefile delete mode 120000 test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c delete mode 120000 test/cbmc/negative_tests/float_overflow_check/Makefile delete mode 120000 test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c delete mode 120000 test/cbmc/negative_tests/float_underflow_check/Makefile delete mode 120000 test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c delete mode 120000 test/cbmc/negative_tests/nan_check/Makefile delete mode 120000 test/cbmc/negative_tests/nan_check/nan_check_harness.c delete mode 120000 test/cbmc/negative_tests/pointer_check/Makefile delete mode 120000 test/cbmc/negative_tests/pointer_check/pointer_check_harness.c delete mode 120000 test/cbmc/negative_tests/pointer_overflow_check/Makefile delete mode 120000 test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c delete mode 120000 test/cbmc/negative_tests/pointer_primitive_check/Makefile delete mode 120000 test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c delete mode 120000 test/cbmc/negative_tests/pointer_underflow_check/Makefile delete mode 120000 test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c delete mode 120000 test/cbmc/negative_tests/signed_overflow_check/Makefile delete mode 120000 test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c delete mode 120000 test/cbmc/negative_tests/signed_underflow_check/Makefile delete mode 120000 test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c delete mode 120000 test/cbmc/negative_tests/undefined_shift_check/Makefile delete mode 120000 test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c delete mode 120000 test/cbmc/negative_tests/unsigned_overflow_check/Makefile delete mode 120000 test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c delete mode 120000 test/cbmc/negative_tests/unsigned_underflow_check/Makefile delete mode 120000 test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c delete mode 100644 test/cbmc/proofs/Makefile-project-defines delete mode 100644 test/cbmc/proofs/Makefile-project-targets delete mode 100644 test/cbmc/proofs/Makefile-project-testing delete mode 100644 test/cbmc/proofs/Makefile-template-defines delete mode 120000 test/cbmc/proofs/Makefile.common delete mode 120000 test/cbmc/proofs/README.md delete mode 120000 test/cbmc/proofs/prepare.py delete mode 100644 test/cbmc/proofs/run-cbmc-proofs.py delete mode 120000 test/cbmc/sources/README.md delete mode 120000 test/cbmc/stubs/README.md diff --git a/test/cbmc/.gitignore b/test/cbmc/.gitignore deleted file mode 100644 index 44240c2..0000000 --- a/test/cbmc/.gitignore +++ /dev/null @@ -1,23 +0,0 @@ -# Emitted when running CBMC proofs -proofs/**/logs -proofs/**/gotos -proofs/**/report -proofs/**/html - -# Emitted by CBMC Viewer -TAGS-* - -# Emitted by Arpa -arpa_cmake/ -arpa-validation-logs/ -Makefile.arpa - -# Emitted by litani -.ninja_deps -.ninja_log -.litani_cache_dir - -# These files should be overwritten whenever prepare.py runs -cbmc-batch.yaml - -__pycache__/ diff --git a/test/cbmc/include/README.md b/test/cbmc/include/README.md deleted file mode 120000 index 4086b9e..0000000 --- a/test/cbmc/include/README.md +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md \ No newline at end of file diff --git a/test/cbmc/negative_tests/README.md b/test/cbmc/negative_tests/README.md deleted file mode 120000 index 60e8d6c..0000000 --- a/test/cbmc/negative_tests/README.md +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/README.md \ No newline at end of file diff --git a/test/cbmc/negative_tests/assert/Makefile b/test/cbmc/negative_tests/assert/Makefile deleted file mode 120000 index f5dc5cb..0000000 --- a/test/cbmc/negative_tests/assert/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/assert/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/assert/assert_harness.c b/test/cbmc/negative_tests/assert/assert_harness.c deleted file mode 120000 index 4405e98..0000000 --- a/test/cbmc/negative_tests/assert/assert_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/assert/assert_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/bounds_check/Makefile b/test/cbmc/negative_tests/bounds_check/Makefile deleted file mode 120000 index da823de..0000000 --- a/test/cbmc/negative_tests/bounds_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/bounds_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/bounds_check/bounds_check_harness.c b/test/cbmc/negative_tests/bounds_check/bounds_check_harness.c deleted file mode 120000 index 5b01436..0000000 --- a/test/cbmc/negative_tests/bounds_check/bounds_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/bounds_check/bounds_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/conversion_check/Makefile b/test/cbmc/negative_tests/conversion_check/Makefile deleted file mode 120000 index 238306b..0000000 --- a/test/cbmc/negative_tests/conversion_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/conversion_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/conversion_check/conversion_check_harness.c b/test/cbmc/negative_tests/conversion_check/conversion_check_harness.c deleted file mode 120000 index 44e9e2c..0000000 --- a/test/cbmc/negative_tests/conversion_check/conversion_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/conversion_check/conversion_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/div_by_zero_check/Makefile b/test/cbmc/negative_tests/div_by_zero_check/Makefile deleted file mode 120000 index 98362b7..0000000 --- a/test/cbmc/negative_tests/div_by_zero_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/div_by_zero_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c b/test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c deleted file mode 120000 index 9351146..0000000 --- a/test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/div_by_zero_check/div_by_zero_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/float_overflow_check/Makefile b/test/cbmc/negative_tests/float_overflow_check/Makefile deleted file mode 120000 index 8a694fc..0000000 --- a/test/cbmc/negative_tests/float_overflow_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_overflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c b/test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c deleted file mode 120000 index b0b7c8b..0000000 --- a/test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_overflow_check/float_overflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/float_underflow_check/Makefile b/test/cbmc/negative_tests/float_underflow_check/Makefile deleted file mode 120000 index a92febc..0000000 --- a/test/cbmc/negative_tests/float_underflow_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_underflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c b/test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c deleted file mode 120000 index ff99ec6..0000000 --- a/test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_underflow_check/float_underflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/nan_check/Makefile b/test/cbmc/negative_tests/nan_check/Makefile deleted file mode 120000 index 4a967a5..0000000 --- a/test/cbmc/negative_tests/nan_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/nan_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/nan_check/nan_check_harness.c b/test/cbmc/negative_tests/nan_check/nan_check_harness.c deleted file mode 120000 index f2e73cb..0000000 --- a/test/cbmc/negative_tests/nan_check/nan_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/nan_check/nan_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_check/Makefile b/test/cbmc/negative_tests/pointer_check/Makefile deleted file mode 120000 index 1134103..0000000 --- a/test/cbmc/negative_tests/pointer_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_check/pointer_check_harness.c b/test/cbmc/negative_tests/pointer_check/pointer_check_harness.c deleted file mode 120000 index c16774a..0000000 --- a/test/cbmc/negative_tests/pointer_check/pointer_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_check/pointer_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_overflow_check/Makefile b/test/cbmc/negative_tests/pointer_overflow_check/Makefile deleted file mode 120000 index cadcbe8..0000000 --- a/test/cbmc/negative_tests/pointer_overflow_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_overflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c b/test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c deleted file mode 120000 index e1ed818..0000000 --- a/test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_primitive_check/Makefile b/test/cbmc/negative_tests/pointer_primitive_check/Makefile deleted file mode 120000 index 7b01588..0000000 --- a/test/cbmc/negative_tests/pointer_primitive_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_primitive_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c b/test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c deleted file mode 120000 index 6c2e2dc..0000000 --- a/test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_underflow_check/Makefile b/test/cbmc/negative_tests/pointer_underflow_check/Makefile deleted file mode 120000 index b05fce3..0000000 --- a/test/cbmc/negative_tests/pointer_underflow_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_underflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c b/test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c deleted file mode 120000 index 06b831d..0000000 --- a/test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/signed_overflow_check/Makefile b/test/cbmc/negative_tests/signed_overflow_check/Makefile deleted file mode 120000 index 5b1e6e1..0000000 --- a/test/cbmc/negative_tests/signed_overflow_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_overflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c b/test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c deleted file mode 120000 index fd74c10..0000000 --- a/test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_overflow_check/signed_overflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/signed_underflow_check/Makefile b/test/cbmc/negative_tests/signed_underflow_check/Makefile deleted file mode 120000 index ed10e0a..0000000 --- a/test/cbmc/negative_tests/signed_underflow_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_underflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c b/test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c deleted file mode 120000 index 0835085..0000000 --- a/test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_underflow_check/signed_underflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/undefined_shift_check/Makefile b/test/cbmc/negative_tests/undefined_shift_check/Makefile deleted file mode 120000 index f6c2cd2..0000000 --- a/test/cbmc/negative_tests/undefined_shift_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/undefined_shift_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c b/test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c deleted file mode 120000 index f4dbf13..0000000 --- a/test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/undefined_shift_check/undefined_shift_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/unsigned_overflow_check/Makefile b/test/cbmc/negative_tests/unsigned_overflow_check/Makefile deleted file mode 120000 index 41fa254..0000000 --- a/test/cbmc/negative_tests/unsigned_overflow_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_overflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c b/test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c deleted file mode 120000 index a0359f9..0000000 --- a/test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/negative_tests/unsigned_underflow_check/Makefile b/test/cbmc/negative_tests/unsigned_underflow_check/Makefile deleted file mode 120000 index e0fc5c4..0000000 --- a/test/cbmc/negative_tests/unsigned_underflow_check/Makefile +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_underflow_check/Makefile \ No newline at end of file diff --git a/test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c b/test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c deleted file mode 120000 index 949db40..0000000 --- a/test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c +++ /dev/null @@ -1 +0,0 @@ -../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c \ No newline at end of file diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines deleted file mode 100644 index f6f7681..0000000 --- a/test/cbmc/proofs/Makefile-project-defines +++ /dev/null @@ -1,37 +0,0 @@ -# -*- mode: makefile -*- -# The first line sets the emacs major mode to Makefile - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -################################################################ -# Use this file to give project-specific definitions of the command -# line arguments to pass to CBMC tools like goto-cc to build the goto -# binaries and cbmc to do the property and coverage checking. -# -# Use this file to override most default definitions of variables in -# Makefile.common. -################################################################ - -# Flags to pass to goto-cc for compilation (typically those passed to gcc -c) -# COMPILE_FLAGS = - -# Flags to pass to goto-cc for linking (typically those passed to gcc) -# LINK_FLAGS = - -# Preprocessor include paths -I... -# Consider adding -# INCLUDES += -I$(CBMC_ROOT)/include -# You will want to decide what order that comes in relative to the other -# include directories in your project. -# -# INCLUDES = - -# Preprocessor definitions -D... -# DEFINES = - -# Path to arpa executable -# ARPA = - -# Flags to pass to cmake for building the project -# ARPA_CMAKE_FLAGS = diff --git a/test/cbmc/proofs/Makefile-project-targets b/test/cbmc/proofs/Makefile-project-targets deleted file mode 100644 index 2d4d460..0000000 --- a/test/cbmc/proofs/Makefile-project-targets +++ /dev/null @@ -1,10 +0,0 @@ -# -*- mode: makefile -*- -# The first line sets the emacs major mode to Makefile - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -################################################################ -# Use this file to give project-specific targets, including targets -# that may depend on targets defined in Makefile.common. -################################################################ diff --git a/test/cbmc/proofs/Makefile-project-testing b/test/cbmc/proofs/Makefile-project-testing deleted file mode 100644 index dc0c209..0000000 --- a/test/cbmc/proofs/Makefile-project-testing +++ /dev/null @@ -1,11 +0,0 @@ -# -*- mode: makefile -*- -# The first line sets the emacs major mode to Makefile - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -################################################################ -# Use this file to define project-specific targets and definitions for -# unit testing or continuous integration that may depend on targets -# defined in Makefile.common -################################################################ diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines deleted file mode 100644 index 0ceb406..0000000 --- a/test/cbmc/proofs/Makefile-template-defines +++ /dev/null @@ -1,19 +0,0 @@ - -# Absolute path to the root of the source tree. -# -SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../source) - - -# Absolute path to the litani script. -# -LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani) - - -# Name of this proof project, displayed in proof reports. For example, -# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots, -# this may be overridden on the command-line to Make, for example -# -# make PROJECT_NAME="FreeRTOS MQTT" report -# -PROJECT_NAME = "coreSNTP" - diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common deleted file mode 120000 index 69d247e..0000000 --- a/test/cbmc/proofs/Makefile.common +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common \ No newline at end of file diff --git a/test/cbmc/proofs/README.md b/test/cbmc/proofs/README.md deleted file mode 120000 index cac5275..0000000 --- a/test/cbmc/proofs/README.md +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md \ No newline at end of file diff --git a/test/cbmc/proofs/prepare.py b/test/cbmc/proofs/prepare.py deleted file mode 120000 index 97c77e9..0000000 --- a/test/cbmc/proofs/prepare.py +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/proofs/prepare.py \ No newline at end of file diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py deleted file mode 100644 index 2a60ab0..0000000 --- a/test/cbmc/proofs/run-cbmc-proofs.py +++ /dev/null @@ -1,259 +0,0 @@ -#!/usr/bin/env python3 -# -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - - -import argparse -import asyncio -import logging -import math -import os -import pathlib -import subprocess -import sys - - -DESCRIPTION = "Configure and run all CBMC proofs in parallel" - -# Keep the epilog hard-wrapped at 70 characters, as it gets printed -# verbatim in the terminal. 70 characters stops here --------------> | -EPILOG = """ -This tool automates the process of running `make report` in each of -the CBMC proof directories. The tool calculates the dependency graph -of all tasks needed to build, run, and report on all the proofs, and -executes these tasks in parallel. - -The tool is roughly equivalent to doing this: - - litani init --project "my-cool-project"; - - find . -name cbmc-proof.txt | while read -r proof; do - pushd $(dirname ${proof}); - - # The `make _report` rule adds a single proof to litani - # without running it - make _report; - - popd; - done - - litani run-build; - -except that it is much faster and provides some convenience options. -The CBMC CI runs this script with no arguments to build and run all -proofs in parallel. The value of "my-cool-project" is taken from the -PROJECT_NAME variable in Makefile-project-defines. - -The --no-standalone argument omits the `litani init` and `litani -run-build`; use it when you want to add additional proof jobs, not -just the CBMC ones. In that case, you would run `litani init` -yourself; then run `run-cbmc-proofs --no-standalone`; add any -additional jobs that you want to execute with `litani add-job`; and -finally run `litani run-build`. -""" - - -def get_project_name(): - cmd = [ - "make", - "-f", "Makefile.common", - "echo-project-name", - ] - logging.debug(" ".join(cmd)) - proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) - if proc.returncode: - logging.critical("could not run make to determine project name") - sys.exit(1) - if not proc.stdout.strip(): - logging.warning( - "project name has not been set; using generic name instead. " - "Set the PROJECT_NAME value in Makefile-project-defines to " - "remove this warning") - return "" - return proc.stdout.strip() - - -def get_args(): - pars = argparse.ArgumentParser( - description=DESCRIPTION, epilog=EPILOG, - formatter_class=argparse.RawDescriptionHelpFormatter) - for arg in [{ - "flags": ["-j", "--parallel-jobs"], - "type": int, - "metavar": "N", - "help": "run at most N proof jobs in parallel", - }, { - "flags": ["--no-standalone"], - "action": "store_true", - "help": "only configure proofs: do not initialize nor run", - }, { - "flags": ["-p", "--proofs"], - "nargs": "+", - "metavar": "DIR", - "help": "only run proof in directory DIR (can pass more than one)", - }, { - "flags": ["--project-name"], - "metavar": "NAME", - "default": get_project_name(), - "help": "project name for report. Default: %(default)s", - }, { - "flags": ["--proof-marker"], - "metavar": "FILE", - "default": "cbmc-proof.txt", - "help": ( - "name of file that marks proof directories. Default: " - "%(default)s"), - }, { - "flags": ["--verbose"], - "action": "store_true", - "help": "verbose output", - }]: - flags = arg.pop("flags") - pars.add_argument(*flags, **arg) - return pars.parse_args() - - -def set_up_logging(verbose): - if verbose: - level = logging.DEBUG - else: - level = logging.WARNING - logging.basicConfig( - format="run-cbmc-proofs: %(message)s", level=level) - - -def task_pool_size(): - ret = os.cpu_count() - if ret is None or ret < 3: - return 1 - return ret - 2 - - -def print_counter(counter): - print( - "\rConfiguring CBMC proofs: " - "{complete:{width}} / {total:{width}}".format( - **counter), end="", file=sys.stderr) - - -def get_proof_dirs(proof_root, proof_list, proof_marker): - if proof_list is not None: - proofs_remaining = list(proof_list) - else: - proofs_remaining = [] - - for root, _, fyles in os.walk(proof_root): - proof_name = str(pathlib.Path(root).name) - if proof_list and proof_name not in proof_list: - continue - if proof_list and proof_name in proofs_remaining: - proofs_remaining.remove(proof_name) - if proof_marker in fyles: - yield root - - if proofs_remaining: - logging.critical( - "The following proofs were not found: %s", - ", ".join(proofs_remaining)) - sys.exit(1) - - -def run_build(litani, jobs): - cmd = [str(litani), "run-build"] - if jobs: - cmd.extend(["-j", str(jobs)]) - - logging.debug(" ".join(cmd)) - proc = subprocess.run(cmd) - if proc.returncode: - logging.critical("Failed to run litani run-build") - sys.exit(1) - - -def get_litani_path(proof_root): - cmd = [ - "make", - "PROOF_ROOT=%s" % proof_root, - "-f", "Makefile.common", - "litani-path", - ] - logging.debug(" ".join(cmd)) - proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) - if proc.returncode: - logging.critical("Could not determine path to litani") - sys.exit(1) - return proc.stdout.strip() - - -async def configure_proof_dirs(queue, counter): - while True: - print_counter(counter) - path = str(await queue.get()) - - proc = await asyncio.create_subprocess_exec( - "nice", "-n", "15", "make", "-B", "--quiet", "_report", cwd=path) - await proc.wait() - counter["fail" if proc.returncode else "pass"].append(path) - counter["complete"] += 1 - - print_counter(counter) - queue.task_done() - - -async def main(): - args = get_args() - set_up_logging(args.verbose) - - proof_root = pathlib.Path(__file__).resolve().parent - litani = get_litani_path(proof_root) - - if not args.no_standalone: - cmd = [str(litani), "init", "--project", args.project_name] - logging.debug(" ".join(cmd)) - proc = subprocess.run(cmd) - if proc.returncode: - logging.critical("Failed to run litani init") - sys.exit(1) - - proof_dirs = list(get_proof_dirs( - proof_root, args.proofs, args.proof_marker)) - if not proof_dirs: - logging.critical("No proof directories found") - sys.exit(1) - - proof_queue = asyncio.Queue() - for proof_dir in proof_dirs: - proof_queue.put_nowait(proof_dir) - - counter = { - "pass": [], - "fail": [], - "complete": 0, - "total": len(proof_dirs), - "width": int(math.log10(len(proof_dirs))) + 1 - } - - tasks = [] - for _ in range(task_pool_size()): - task = asyncio.create_task(configure_proof_dirs( - proof_queue, counter)) - tasks.append(task) - - await proof_queue.join() - - print_counter(counter) - print("", file=sys.stderr) - - if counter["fail"]: - logging.critical( - "Failed to configure the following proofs:\n%s", "\n".join( - [str(f) for f in counter["fail"]])) - sys.exit(1) - - if not args.no_standalone: - run_build(litani, args.parallel_jobs) - - -if __name__ == "__main__": - asyncio.run(main()) diff --git a/test/cbmc/sources/README.md b/test/cbmc/sources/README.md deleted file mode 120000 index 969d1de..0000000 --- a/test/cbmc/sources/README.md +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/sources/README.md \ No newline at end of file diff --git a/test/cbmc/stubs/README.md b/test/cbmc/stubs/README.md deleted file mode 120000 index 327d6f6..0000000 --- a/test/cbmc/stubs/README.md +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/stubs/README.md \ No newline at end of file From a4548d5130b81a832e9b9a773aaa42eb24f308c2 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Fri, 7 May 2021 11:30:23 -0700 Subject: [PATCH 05/44] Sntp_ConvertToUnixTime CBMC PROOF --- .../proofs/Sntp_ConvertToUnixTime/Makefile | 20 ++++++++++ .../proofs/Sntp_ConvertToUnixTime/README.md | 23 +++++++++++ .../Sntp_ConvertToUnixTime_harness.c | 40 +++++++++++++++++++ ...ntp_ConvertToUnixTime_harness.c.uncrustify | 40 +++++++++++++++++++ .../Sntp_ConvertToUnixTime/cbmc-proof.txt | 1 + .../Sntp_ConvertToUnixTime/cbmc-viewer.json | 7 ++++ 6 files changed, 131 insertions(+) create mode 100644 test/cbmc/proofs/Sntp_ConvertToUnixTime/Makefile create mode 100644 test/cbmc/proofs/Sntp_ConvertToUnixTime/README.md create mode 100644 test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c create mode 100644 test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c.uncrustify create mode 100644 test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-proof.txt create mode 100644 test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-viewer.json diff --git a/test/cbmc/proofs/Sntp_ConvertToUnixTime/Makefile b/test/cbmc/proofs/Sntp_ConvertToUnixTime/Makefile new file mode 100644 index 0000000..3f68464 --- /dev/null +++ b/test/cbmc/proofs/Sntp_ConvertToUnixTime/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_ConvertToUnixTime_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_ConvertToUnixTime + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_serializer.c + +include ../Makefile.common diff --git a/test/cbmc/proofs/Sntp_ConvertToUnixTime/README.md b/test/cbmc/proofs/Sntp_ConvertToUnixTime/README.md new file mode 100644 index 0000000..3bf0834 --- /dev/null +++ b/test/cbmc/proofs/Sntp_ConvertToUnixTime/README.md @@ -0,0 +1,23 @@ +Sntp_ConvertToUnixTime proof +============== + +This directory contains a memory safety proof for Sntp_ConvertToUnixTime. + +The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of: + * Sntp_ConvertToUnixTime() + +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`). diff --git a/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c b/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c new file mode 100644 index 0000000..b7769a2 --- /dev/null +++ b/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c @@ -0,0 +1,40 @@ +/* + * 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_ConvertToUnixTime_harness.c + * @brief Implements the proof harness for Sntp_ConvertToUnixTime function. + */ + +#include "core_sntp_serializer.h" + +void harness() +{ + SntpTimestamp_t sntpTime; + uint32_t unixTimeSecs; + uint32_t unixTimeMicrosecs; + SntpStatus_t sntpStatus; + + sntpStatus = Sntp_ConvertToUnixTime( &sntpTime, &unixTimeSecs, &unixTimeMicrosecs ); + + __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpErrorTimeNotSupported || sntpStatus == SntpSuccess ), "The return value is not a valid SNTP Status" ); +} diff --git a/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c.uncrustify b/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c.uncrustify new file mode 100644 index 0000000..b7769a2 --- /dev/null +++ b/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c.uncrustify @@ -0,0 +1,40 @@ +/* + * 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_ConvertToUnixTime_harness.c + * @brief Implements the proof harness for Sntp_ConvertToUnixTime function. + */ + +#include "core_sntp_serializer.h" + +void harness() +{ + SntpTimestamp_t sntpTime; + uint32_t unixTimeSecs; + uint32_t unixTimeMicrosecs; + SntpStatus_t sntpStatus; + + sntpStatus = Sntp_ConvertToUnixTime( &sntpTime, &unixTimeSecs, &unixTimeMicrosecs ); + + __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpErrorTimeNotSupported || sntpStatus == SntpSuccess ), "The return value is not a valid SNTP Status" ); +} diff --git a/test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-proof.txt b/test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-proof.txt new file mode 100644 index 0000000..6ed46f1 --- /dev/null +++ b/test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-viewer.json b/test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-viewer.json new file mode 100644 index 0000000..06b60b7 --- /dev/null +++ b/test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "Sntp_ConvertToUnixTime", + "proof-root": "test/cbmc/proofs" +} From 7c0b79377ecba22905890e30f773544c57df0ef5 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Fri, 7 May 2021 13:06:16 -0700 Subject: [PATCH 06/44] removing uncrstify file --- ...ntp_ConvertToUnixTime_harness.c.uncrustify | 40 ------------------- 1 file changed, 40 deletions(-) delete mode 100644 test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c.uncrustify diff --git a/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c.uncrustify b/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c.uncrustify deleted file mode 100644 index b7769a2..0000000 --- a/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c.uncrustify +++ /dev/null @@ -1,40 +0,0 @@ -/* - * 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_ConvertToUnixTime_harness.c - * @brief Implements the proof harness for Sntp_ConvertToUnixTime function. - */ - -#include "core_sntp_serializer.h" - -void harness() -{ - SntpTimestamp_t sntpTime; - uint32_t unixTimeSecs; - uint32_t unixTimeMicrosecs; - SntpStatus_t sntpStatus; - - sntpStatus = Sntp_ConvertToUnixTime( &sntpTime, &unixTimeSecs, &unixTimeMicrosecs ); - - __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpErrorTimeNotSupported || sntpStatus == SntpSuccess ), "The return value is not a valid SNTP Status" ); -} From c8dc9d829cf9bb517f79363559ed7e404e1a6689 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Fri, 7 May 2021 15:43:33 -0700 Subject: [PATCH 07/44] Address Feedback --- .../Sntp_ConvertToUnixTime_harness.c | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c b/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c index b7769a2..18c89e7 100644 --- a/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c +++ b/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c @@ -29,12 +29,16 @@ void harness() { - SntpTimestamp_t sntpTime; - uint32_t unixTimeSecs; - uint32_t unixTimeMicrosecs; + SntpTimestamp_t * pSntpTime; + uint32_t * pUnixTimeSecs; + uint32_t * pUnixTimeMicrosecs; SntpStatus_t sntpStatus; - sntpStatus = Sntp_ConvertToUnixTime( &sntpTime, &unixTimeSecs, &unixTimeMicrosecs ); + pSntpTime = malloc( sizeof( SntpTimestamp_t ) ); + pUnixTimeSecs = malloc( sizeof( uint32_t ) ); + pUnixTimeMicrosecs = malloc( sizeof( uint32_t ) ); + + sntpStatus = Sntp_ConvertToUnixTime( pSntpTime, pUnixTimeSecs, pUnixTimeMicrosecs ); __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpErrorTimeNotSupported || sntpStatus == SntpSuccess ), "The return value is not a valid SNTP Status" ); } From d6e4457135ed70150ca5de7a7739b3d7940e3b30 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Fri, 7 May 2021 15:47:51 -0700 Subject: [PATCH 08/44] Allocation changes in poll Interval proof --- .../Sntp_CalculatePollInterval_harness.c | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/test/cbmc/proofs/Sntp_CalculatePollInterval/Sntp_CalculatePollInterval_harness.c b/test/cbmc/proofs/Sntp_CalculatePollInterval/Sntp_CalculatePollInterval_harness.c index 1770b9b..f56e45b 100644 --- a/test/cbmc/proofs/Sntp_CalculatePollInterval/Sntp_CalculatePollInterval_harness.c +++ b/test/cbmc/proofs/Sntp_CalculatePollInterval/Sntp_CalculatePollInterval_harness.c @@ -31,10 +31,11 @@ void harness() { uint16_t clockFreqTolerance; uint16_t desiredAccuracy; - uint32_t pollInterval; + uint32_t * pPollInterval; SntpStatus_t sntpStatus; - sntpStatus = Sntp_CalculatePollInterval( clockFreqTolerance, desiredAccuracy, &pollInterval ); + pPollInterval = malloc( sizeof( uint32_t ) ); + sntpStatus = Sntp_CalculatePollInterval( clockFreqTolerance, desiredAccuracy, pPollInterval ); __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpSuccess || sntpStatus == SntpZeroPollInterval ), "The return value is not a valid SNTP status." ); } From c1f5b2d81b26a3cfc8ea4ad7fcf1f58768556773 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Mon, 10 May 2021 18:58:40 -0700 Subject: [PATCH 09/44] Sntp_Init CBMC PROOF --- test/cbmc/proofs/Sntp_Init/Makefile | 20 +++++++ test/cbmc/proofs/Sntp_Init/README.md | 23 ++++++++ .../cbmc/proofs/Sntp_Init/Sntp_Init_harness.c | 56 +++++++++++++++++++ test/cbmc/proofs/Sntp_Init/cbmc-proof.txt | 1 + test/cbmc/proofs/Sntp_Init/cbmc-viewer.json | 7 +++ 5 files changed, 107 insertions(+) create mode 100644 test/cbmc/proofs/Sntp_Init/Makefile create mode 100644 test/cbmc/proofs/Sntp_Init/README.md create mode 100644 test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c create mode 100644 test/cbmc/proofs/Sntp_Init/cbmc-proof.txt create mode 100644 test/cbmc/proofs/Sntp_Init/cbmc-viewer.json diff --git a/test/cbmc/proofs/Sntp_Init/Makefile b/test/cbmc/proofs/Sntp_Init/Makefile new file mode 100644 index 0000000..ca3644a --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/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_Init_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_Init + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_client.c + +include ../Makefile.common diff --git a/test/cbmc/proofs/Sntp_Init/README.md b/test/cbmc/proofs/Sntp_Init/README.md new file mode 100644 index 0000000..b5a9a27 --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/README.md @@ -0,0 +1,23 @@ +Sntp_Init proof +============== + +This directory contains a memory safety proof for Sntp_Init. + +The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of: + * Sntp_Init() + +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`). diff --git a/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c b/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c new file mode 100644 index 0000000..e6b3bf9 --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c @@ -0,0 +1,56 @@ +/* + * 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_Init_harness.c + * @brief Implements the proof harness for Sntp_Init function. + */ + +#include +#include "core_sntp_client.h" + +void harness() +{ + SntpContext_t * pContext; + SntpServerInfo_t * pTimeServers; + size_t numOfServers; + uint8_t * pNetworkBuffer; + size_t bufferSize; + SntpResolveDns_t resolveDnsFunc; + SntpGetTime_t getSystemTimeFunc; + SntpSetTime_t setSystemTimeFunc; + UdpTransportInterface_t * pTransportIntf; + SntpAuthenticationInterface_t * pAuthIntf; + SntpStatus_t sntpStatus; + + pContext = malloc( sizeof( SntpContext_t ) ); + pTimeServers = malloc( sizeof( SntpServerInfo_t ) ); + pNetworkBuffer = malloc( sizeof( uint8_t ) ); + pTransportIntf = malloc( sizeof( UdpTransportInterface_t ) ); + pAuthIntf = malloc( sizeof( SntpAuthenticationInterface_t ) ); + + sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, pNetworkBuffer, + bufferSize, resolveDnsFunc, getSystemTimeFunc, setSystemTimeFunc, + pTransportIntf, pAuthIntf ); + + __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpSuccess ), "The return value is not a valid SNTP Status" ); +} diff --git a/test/cbmc/proofs/Sntp_Init/cbmc-proof.txt b/test/cbmc/proofs/Sntp_Init/cbmc-proof.txt new file mode 100644 index 0000000..6ed46f1 --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/Sntp_Init/cbmc-viewer.json b/test/cbmc/proofs/Sntp_Init/cbmc-viewer.json new file mode 100644 index 0000000..d33d55e --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "Sntp_Init", + "proof-root": "test/cbmc/proofs" +} From d6fa78d8a1b7743ab242500c7d9f77a1608a38b7 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Mon, 10 May 2021 18:58:40 -0700 Subject: [PATCH 10/44] Sntp_Init CBMC PROOF --- test/cbmc/proofs/Sntp_Init/Makefile | 20 +++++++ test/cbmc/proofs/Sntp_Init/README.md | 23 ++++++++ .../cbmc/proofs/Sntp_Init/Sntp_Init_harness.c | 56 +++++++++++++++++++ test/cbmc/proofs/Sntp_Init/cbmc-proof.txt | 1 + test/cbmc/proofs/Sntp_Init/cbmc-viewer.json | 7 +++ 5 files changed, 107 insertions(+) create mode 100644 test/cbmc/proofs/Sntp_Init/Makefile create mode 100644 test/cbmc/proofs/Sntp_Init/README.md create mode 100644 test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c create mode 100644 test/cbmc/proofs/Sntp_Init/cbmc-proof.txt create mode 100644 test/cbmc/proofs/Sntp_Init/cbmc-viewer.json diff --git a/test/cbmc/proofs/Sntp_Init/Makefile b/test/cbmc/proofs/Sntp_Init/Makefile new file mode 100644 index 0000000..ca3644a --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/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_Init_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_Init + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_client.c + +include ../Makefile.common diff --git a/test/cbmc/proofs/Sntp_Init/README.md b/test/cbmc/proofs/Sntp_Init/README.md new file mode 100644 index 0000000..b5a9a27 --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/README.md @@ -0,0 +1,23 @@ +Sntp_Init proof +============== + +This directory contains a memory safety proof for Sntp_Init. + +The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of: + * Sntp_Init() + +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`). diff --git a/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c b/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c new file mode 100644 index 0000000..e6b3bf9 --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c @@ -0,0 +1,56 @@ +/* + * 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_Init_harness.c + * @brief Implements the proof harness for Sntp_Init function. + */ + +#include +#include "core_sntp_client.h" + +void harness() +{ + SntpContext_t * pContext; + SntpServerInfo_t * pTimeServers; + size_t numOfServers; + uint8_t * pNetworkBuffer; + size_t bufferSize; + SntpResolveDns_t resolveDnsFunc; + SntpGetTime_t getSystemTimeFunc; + SntpSetTime_t setSystemTimeFunc; + UdpTransportInterface_t * pTransportIntf; + SntpAuthenticationInterface_t * pAuthIntf; + SntpStatus_t sntpStatus; + + pContext = malloc( sizeof( SntpContext_t ) ); + pTimeServers = malloc( sizeof( SntpServerInfo_t ) ); + pNetworkBuffer = malloc( sizeof( uint8_t ) ); + pTransportIntf = malloc( sizeof( UdpTransportInterface_t ) ); + pAuthIntf = malloc( sizeof( SntpAuthenticationInterface_t ) ); + + sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, pNetworkBuffer, + bufferSize, resolveDnsFunc, getSystemTimeFunc, setSystemTimeFunc, + pTransportIntf, pAuthIntf ); + + __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpSuccess ), "The return value is not a valid SNTP Status" ); +} diff --git a/test/cbmc/proofs/Sntp_Init/cbmc-proof.txt b/test/cbmc/proofs/Sntp_Init/cbmc-proof.txt new file mode 100644 index 0000000..6ed46f1 --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/Sntp_Init/cbmc-viewer.json b/test/cbmc/proofs/Sntp_Init/cbmc-viewer.json new file mode 100644 index 0000000..d33d55e --- /dev/null +++ b/test/cbmc/proofs/Sntp_Init/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "Sntp_Init", + "proof-root": "test/cbmc/proofs" +} From 274f2879143f1941bcfbb8bdfc237e8ff3b93c97 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 13:19:32 -0700 Subject: [PATCH 11/44] Addressing Feedback --- test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c b/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c index e6b3bf9..5351630 100644 --- a/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c +++ b/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c @@ -44,7 +44,10 @@ void harness() pContext = malloc( sizeof( SntpContext_t ) ); pTimeServers = malloc( sizeof( SntpServerInfo_t ) ); - pNetworkBuffer = malloc( sizeof( uint8_t ) ); + + __CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE ); + + pNetworkBuffer = malloc( bufferSize ); pTransportIntf = malloc( sizeof( UdpTransportInterface_t ) ); pAuthIntf = malloc( sizeof( SntpAuthenticationInterface_t ) ); @@ -52,5 +55,5 @@ void harness() bufferSize, resolveDnsFunc, getSystemTimeFunc, setSystemTimeFunc, pTransportIntf, pAuthIntf ); - __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpSuccess ), "The return value is not a valid SNTP Status" ); + __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpSuccess || sntpStatus == SntpErrorBufferTooSmall ), "The return value is not a valid SNTP Status" ); } From 29bea0206806105d0f6325f19853f180910ce198 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 15:29:45 -0700 Subject: [PATCH 12/44] Sntp_DeserializeResponse Proof --- source/core_sntp_serializer.c | 5 ++ .../proofs/Sntp_DeserializeResponse/Makefile | 20 +++++++ .../proofs/Sntp_DeserializeResponse/README.md | 23 ++++++++ .../Sntp_DeserializeResponse_harness.c | 53 +++++++++++++++++++ .../Sntp_DeserializeResponse/cbmc-proof.txt | 1 + .../Sntp_DeserializeResponse/cbmc-viewer.json | 7 +++ 6 files changed, 109 insertions(+) create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/Makefile create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/README.md create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/Sntp_DeserializeResponse_harness.c create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-proof.txt create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-viewer.json diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c index cb92c97..53f4292 100644 --- a/source/core_sntp_serializer.c +++ b/source/core_sntp_serializer.c @@ -32,6 +32,8 @@ /* Include API header. */ #include "core_sntp_serializer.h" +#pragma CPROVER check disable "unsigned-overflow" +#pragma CPROVER check disable "conversion" /** * @brief The version of SNTP supported by the coreSNTP library by complying @@ -267,6 +269,8 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime, assert( pClientRxTime != NULL ); assert( pClockOffset != NULL ); + #pragma CPROVER check push + /* Calculate a sample first order difference value between the * server and system timestamps. */ firstOrderDiff = pClientRxTime->seconds - pServerTxTime->seconds; @@ -312,6 +316,7 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime, status = SntpClockOffsetOverflow; } + #pragma CPROVER check pop return status; } diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/Makefile b/test/cbmc/proofs/Sntp_DeserializeResponse/Makefile new file mode 100644 index 0000000..68eef70 --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/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_DeserializeResponse_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_DeserializeResponse + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_serializer.c + +include ../Makefile.common diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/README.md b/test/cbmc/proofs/Sntp_DeserializeResponse/README.md new file mode 100644 index 0000000..930771c --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/README.md @@ -0,0 +1,23 @@ +Sntp_DeserializeResponse proof +============== + +This directory contains a memory safety proof for Sntp_DeserializeResponse. + +The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of: + * Sntp_DeserializeResponse() + +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`). diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/Sntp_DeserializeResponse_harness.c b/test/cbmc/proofs/Sntp_DeserializeResponse/Sntp_DeserializeResponse_harness.c new file mode 100644 index 0000000..955211c --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/Sntp_DeserializeResponse_harness.c @@ -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 Sntp_DeserializeResponse_harness.c + * @brief Implements the proof harness for Sntp_DeserializeResponse function. + */ + +#include +#include "core_sntp_serializer.h" + +void harness() +{ + SntpTimestamp_t * pRequestTime; + SntpTimestamp_t * pResponseRxTime; + void * pResponseBuffer; + size_t bufferSize; + SntpResponseData_t * pParsedResponse; + SntpStatus_t sntpStatus; + + __CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE ); + + pRequestTime = malloc( sizeof( SntpTimestamp_t ) ); + pResponseRxTime = malloc( sizeof( SntpTimestamp_t ) ); + pResponseBuffer = malloc( bufferSize ); + pParsedResponse = malloc( sizeof( SntpResponseData_t ) ); + + sntpStatus = Sntp_DeserializeResponse( pRequestTime, pResponseRxTime, pResponseBuffer, bufferSize, pParsedResponse ); + + __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter ) || ( sntpStatus == SntpErrorBufferTooSmall ) || + ( sntpStatus == SntpInvalidResponse ) || ( sntpStatus == SntpSuccess ) || ( sntpStatus == SntpRejectedResponseChangeServer ) || + ( sntpStatus == SntpRejectedResponseRetryWithBackoff ) || ( sntpStatus == SntpRejectedResponseOtherCode ) || + ( sntpStatus == SntpClockOffsetOverflow ), "This is a valid sntp return status" ); +} diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-proof.txt b/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-proof.txt new file mode 100644 index 0000000..6ed46f1 --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-viewer.json b/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-viewer.json new file mode 100644 index 0000000..db54192 --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "Sntp_DeserializeResponse", + "proof-root": "test/cbmc/proofs" +} From 9a17a76300b924756b969a2fe47ee0c4748f6b6d Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 16:59:12 -0700 Subject: [PATCH 13/44] ci.yml changes --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ff1d9a1..debac62 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -17,6 +17,7 @@ jobs: -G "Unix Makefiles" \ -DCMAKE_BUILD_TYPE=Debug \ -DBUILD_CLONE_SUBMODULES=ON \ + -Wno-error=unknown-pragmas \ -DCMAKE_C_FLAGS='-Wall -Wextra -Werror' make -C build/ coverity_analysis -j8 - name: Build Library in Release mode From cef51b496d92651a21da79f6b2272cbfdf1c17ed Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 17:02:18 -0700 Subject: [PATCH 14/44] ci.yml changes --- .github/workflows/ci.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index debac62..39d748c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -17,8 +17,7 @@ jobs: -G "Unix Makefiles" \ -DCMAKE_BUILD_TYPE=Debug \ -DBUILD_CLONE_SUBMODULES=ON \ - -Wno-error=unknown-pragmas \ - -DCMAKE_C_FLAGS='-Wall -Wextra -Werror' + -DCMAKE_C_FLAGS='-Wall -Wextra -Werror -Wno-error=unknown-pragmas' make -C build/ coverity_analysis -j8 - name: Build Library in Release mode run: | From c83694422ed083609aca825cd0a8848471b89744 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 17:08:17 -0700 Subject: [PATCH 15/44] ci.yml changes --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 39d748c..1e231c3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,7 +25,7 @@ jobs: cmake -S test -B build/ -G "Unix Makefiles" \ -DCMAKE_BUILD_TYPE=Release \ -DBUILD_CLONE_SUBMODULES=ON \ - -DCMAKE_C_FLAGS='-Wall -Wextra -Werror -DNDEBUG' + -DCMAKE_C_FLAGS='-Wall -Wextra -Werror -Wno-error=unknown-pragmas -DNDEBUG' make -C build/ coverity_analysis -j8 unittest-and-coverage: runs-on: ubuntu-latest From 42afe31a8829e4f794d3d5c9ef2862b5c8a3a50d Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 17:11:21 -0700 Subject: [PATCH 16/44] ci.yml changes --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1e231c3..58ea638 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -39,7 +39,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: | From 7e24bb917d6a7ec567684c461225a6b8e4c1bb91 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 15:29:45 -0700 Subject: [PATCH 17/44] Sntp_DeserializeResponse Proof --- source/core_sntp_serializer.c | 5 ++ .../proofs/Sntp_DeserializeResponse/Makefile | 20 +++++++ .../proofs/Sntp_DeserializeResponse/README.md | 23 ++++++++ .../Sntp_DeserializeResponse_harness.c | 53 +++++++++++++++++++ .../Sntp_DeserializeResponse/cbmc-proof.txt | 1 + .../Sntp_DeserializeResponse/cbmc-viewer.json | 7 +++ 6 files changed, 109 insertions(+) create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/Makefile create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/README.md create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/Sntp_DeserializeResponse_harness.c create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-proof.txt create mode 100644 test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-viewer.json diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c index cb92c97..53f4292 100644 --- a/source/core_sntp_serializer.c +++ b/source/core_sntp_serializer.c @@ -32,6 +32,8 @@ /* Include API header. */ #include "core_sntp_serializer.h" +#pragma CPROVER check disable "unsigned-overflow" +#pragma CPROVER check disable "conversion" /** * @brief The version of SNTP supported by the coreSNTP library by complying @@ -267,6 +269,8 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime, assert( pClientRxTime != NULL ); assert( pClockOffset != NULL ); + #pragma CPROVER check push + /* Calculate a sample first order difference value between the * server and system timestamps. */ firstOrderDiff = pClientRxTime->seconds - pServerTxTime->seconds; @@ -312,6 +316,7 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime, status = SntpClockOffsetOverflow; } + #pragma CPROVER check pop return status; } diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/Makefile b/test/cbmc/proofs/Sntp_DeserializeResponse/Makefile new file mode 100644 index 0000000..68eef70 --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/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_DeserializeResponse_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_DeserializeResponse + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_serializer.c + +include ../Makefile.common diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/README.md b/test/cbmc/proofs/Sntp_DeserializeResponse/README.md new file mode 100644 index 0000000..930771c --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/README.md @@ -0,0 +1,23 @@ +Sntp_DeserializeResponse proof +============== + +This directory contains a memory safety proof for Sntp_DeserializeResponse. + +The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of: + * Sntp_DeserializeResponse() + +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`). diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/Sntp_DeserializeResponse_harness.c b/test/cbmc/proofs/Sntp_DeserializeResponse/Sntp_DeserializeResponse_harness.c new file mode 100644 index 0000000..955211c --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/Sntp_DeserializeResponse_harness.c @@ -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 Sntp_DeserializeResponse_harness.c + * @brief Implements the proof harness for Sntp_DeserializeResponse function. + */ + +#include +#include "core_sntp_serializer.h" + +void harness() +{ + SntpTimestamp_t * pRequestTime; + SntpTimestamp_t * pResponseRxTime; + void * pResponseBuffer; + size_t bufferSize; + SntpResponseData_t * pParsedResponse; + SntpStatus_t sntpStatus; + + __CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE ); + + pRequestTime = malloc( sizeof( SntpTimestamp_t ) ); + pResponseRxTime = malloc( sizeof( SntpTimestamp_t ) ); + pResponseBuffer = malloc( bufferSize ); + pParsedResponse = malloc( sizeof( SntpResponseData_t ) ); + + sntpStatus = Sntp_DeserializeResponse( pRequestTime, pResponseRxTime, pResponseBuffer, bufferSize, pParsedResponse ); + + __CPROVER_assert( ( sntpStatus == SntpErrorBadParameter ) || ( sntpStatus == SntpErrorBufferTooSmall ) || + ( sntpStatus == SntpInvalidResponse ) || ( sntpStatus == SntpSuccess ) || ( sntpStatus == SntpRejectedResponseChangeServer ) || + ( sntpStatus == SntpRejectedResponseRetryWithBackoff ) || ( sntpStatus == SntpRejectedResponseOtherCode ) || + ( sntpStatus == SntpClockOffsetOverflow ), "This is a valid sntp return status" ); +} diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-proof.txt b/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-proof.txt new file mode 100644 index 0000000..6ed46f1 --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-viewer.json b/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-viewer.json new file mode 100644 index 0000000..db54192 --- /dev/null +++ b/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "Sntp_DeserializeResponse", + "proof-root": "test/cbmc/proofs" +} From 43e6d4698dc7b4d49e8f463f0da880ebb3ab7f6e Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 16:59:12 -0700 Subject: [PATCH 18/44] ci.yml changes --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ff1d9a1..debac62 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -17,6 +17,7 @@ jobs: -G "Unix Makefiles" \ -DCMAKE_BUILD_TYPE=Debug \ -DBUILD_CLONE_SUBMODULES=ON \ + -Wno-error=unknown-pragmas \ -DCMAKE_C_FLAGS='-Wall -Wextra -Werror' make -C build/ coverity_analysis -j8 - name: Build Library in Release mode From ed062b9fa37e30989a8de32112f5c797e133d4bc Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 17:02:18 -0700 Subject: [PATCH 19/44] ci.yml changes --- .github/workflows/ci.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index debac62..39d748c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -17,8 +17,7 @@ jobs: -G "Unix Makefiles" \ -DCMAKE_BUILD_TYPE=Debug \ -DBUILD_CLONE_SUBMODULES=ON \ - -Wno-error=unknown-pragmas \ - -DCMAKE_C_FLAGS='-Wall -Wextra -Werror' + -DCMAKE_C_FLAGS='-Wall -Wextra -Werror -Wno-error=unknown-pragmas' make -C build/ coverity_analysis -j8 - name: Build Library in Release mode run: | From 4352bf16836476adfc5382db43b2787e8fcb9fa6 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 17:08:17 -0700 Subject: [PATCH 20/44] ci.yml changes --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 39d748c..1e231c3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,7 +25,7 @@ jobs: cmake -S test -B build/ -G "Unix Makefiles" \ -DCMAKE_BUILD_TYPE=Release \ -DBUILD_CLONE_SUBMODULES=ON \ - -DCMAKE_C_FLAGS='-Wall -Wextra -Werror -DNDEBUG' + -DCMAKE_C_FLAGS='-Wall -Wextra -Werror -Wno-error=unknown-pragmas -DNDEBUG' make -C build/ coverity_analysis -j8 unittest-and-coverage: runs-on: ubuntu-latest From 3bd6a3bf75b80bd6e17fcb4e05b978bc1cc58fd2 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Tue, 11 May 2021 17:11:21 -0700 Subject: [PATCH 21/44] ci.yml changes --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1e231c3..58ea638 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -39,7 +39,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: | From 12ff596f83afcc39afde39b3f6953fbddcac8e92 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Wed, 12 May 2021 17:39:20 -0700 Subject: [PATCH 22/44] Updating execute permissions on run-cbmc-proofs.py --- test/cbmc/proofs/run-cbmc-proofs.py | 0 1 file changed, 0 insertions(+), 0 deletions(-) mode change 100644 => 100755 test/cbmc/proofs/run-cbmc-proofs.py diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py old mode 100644 new mode 100755 From 439d7e1a44303b2d524301cdd8d4e5bb2e05bda7 Mon Sep 17 00:00:00 2001 From: Archit Aggarwal Date: Thu, 13 May 2021 01:08:23 +0000 Subject: [PATCH 23/44] 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 Date: Thu, 13 May 2021 01:19:59 +0000 Subject: [PATCH 24/44] 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 Date: Thu, 13 May 2021 01:22:34 +0000 Subject: [PATCH 25/44] 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 Date: Thu, 13 May 2021 01:31:35 +0000 Subject: [PATCH 26/44] 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 Date: Thu, 13 May 2021 02:09:42 +0000 Subject: [PATCH 27/44] 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 Date: Thu, 13 May 2021 02:20:18 +0000 Subject: [PATCH 28/44] 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 Date: Thu, 13 May 2021 02:34:47 +0000 Subject: [PATCH 29/44] 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 Date: Thu, 13 May 2021 02:37:08 +0000 Subject: [PATCH 30/44] 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 Date: Thu, 13 May 2021 22:07:56 +0000 Subject: [PATCH 31/44] 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 Date: Thu, 13 May 2021 23:29:34 +0000 Subject: [PATCH 32/44] 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 Date: Thu, 13 May 2021 23:36:09 +0000 Subject: [PATCH 33/44] 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 Date: Thu, 13 May 2021 23:55:42 +0000 Subject: [PATCH 34/44] 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 Date: Fri, 14 May 2021 00:03:18 +0000 Subject: [PATCH 35/44] 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 b4d90ae6482a3f5cdbf40c3ff06b6f4a6302ba72 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 13 May 2021 18:35:21 -0700 Subject: [PATCH 36/44] Sntp_SendTimeRequest proof --- test/cbmc/include/core_sntp_cbmc_state.h | 53 +++++++ test/cbmc/include/core_sntp_config.h | 175 ++++++++++++++++++++++ test/cbmc/include/core_sntp_stubs.h | 137 +++++++++++++++++ test/cbmc/sources/core_sntp_cbmc_state.c | 113 ++++++++++++++ test/cbmc/stubs/core_sntp_stubs.c | 183 +++++++++++++++++++++++ 5 files changed, 661 insertions(+) create mode 100644 test/cbmc/include/core_sntp_cbmc_state.h create mode 100644 test/cbmc/include/core_sntp_config.h create mode 100644 test/cbmc/include/core_sntp_stubs.h create mode 100644 test/cbmc/sources/core_sntp_cbmc_state.c create mode 100644 test/cbmc/stubs/core_sntp_stubs.c diff --git a/test/cbmc/include/core_sntp_cbmc_state.h b/test/cbmc/include/core_sntp_cbmc_state.h new file mode 100644 index 0000000..64900bf --- /dev/null +++ b/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_ */ diff --git a/test/cbmc/include/core_sntp_config.h b/test/cbmc/include/core_sntp_config.h new file mode 100644 index 0000000..2ee1a39 --- /dev/null +++ b/test/cbmc/include/core_sntp_config.h @@ -0,0 +1,175 @@ +/* + * coreSNTP v1.0.0 + * Copyright (C) 2020 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_config_defaults.h + * @brief This file represents the default values for the configuration macros + * of the coreSNTP library. + * + * @note This file SHOULD NOT be modified. If custom values are needed for + * any configuration macro, a core_sntp_config.h file should be provided to + * the SNTP library to override the default values defined in this file. + * To build the library with the core_sntp_config.h file, make sure to + * not set the SNTP_DO_NOT_USE_CUSTOM_CONFIG preprocessor macro. + */ + +#ifndef CORE_SNTP_CONFIG_DEFAULTS_H_ +#define CORE_SNTP_CONFIG_DEFAULTS_H_ + +/* The macro definition for SNTP_DO_NOT_USE_CUSTOM_CONFIG is for Doxygen + * documentation only. */ + +/** + * @brief Define this macro to build the SNTP library without the custom config + * file core_sntp_config.h. + * + * Without the custom config, the SNTP library builds with + * default values of config macros defined in core_sntp_config_defaults.h file. + * + * If a custom config is provided, then SNTP_DO_NOT_USE_CUSTOM_CONFIG should not + * be defined. + */ +#ifdef DOXYGEN + #define SNTP_DO_NOT_USE_CUSTOM_CONFIG +#endif + +/** + * @brief The maximum duration between non-empty network reads while + * receiving an SNTP packet via the #Sntp_ReceiveTimeResponse API function. + * + * When an incoming SNTP packet is detected, the transport receive function + * may be called multiple times until all of the expected number of bytes of the + * packet are received. This timeout represents the maximum polling duration that + * is allowed without any data reception from the network for the incoming packet. + * + * If the timeout expires, the #Sntp_ReceiveTimeResponse function will return + * #SntpErrorNetworkFailure. + * + * Possible values: Any positive 16 bit integer. Recommended to use a + * small timeout value.
+ * Default value: `10` + */ +#ifndef SNTP_RECV_POLLING_TIMEOUT_MS + #define SNTP_RECV_POLLING_TIMEOUT_MS ( 10U ) +#endif + +/** + * @brief The maximum duration between non-empty network transmissions while + * sending an SNTP packet via the #Sntp_SendTimeRequest API function. + * + * When sending an SNTP packet, the transport send function may be called multiple + * times until all of the required number of bytes are sent. + * This timeout represents the maximum duration that is allowed for no data + * transmission over the network through the transport send function. + * + * If the timeout expires, the #Sntp_SendTimeRequest function will return + * #SntpErrorNetworkFailure. + * + * Possible values: Any positive 16 bit integer. Recommended to use a small + * timeout value.
+ * Default value: `10` + */ +#ifndef SNTP_SEND_RETRY_TIMEOUT_MS + #define SNTP_SEND_RETRY_TIMEOUT_MS ( 10U ) +#endif + +/** + * @brief Macro that is called in the SNTP library for logging "Error" level + * messages. + * + * To enable error level logging in the SNTP library, this macro should be mapped to the + * application-specific logging implementation that supports error logging. + * + * @note This logging macro is called in the SNTP library with parameters wrapped in + * double parentheses to be ISO C89/C90 standard compliant. For a reference + * POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the + * logging-stack in demos folder of the + * [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C). + * + * Default value: Error logging is turned off, and no code is generated for calls + * to the macro in the SNTP library on compilation. + */ +#ifndef LogError + #define LogError( message ) +#endif + +/** + * @brief Macro that is called in the SNTP library for logging "Warning" level + * messages. + * + * To enable warning level logging in the SNTP library, this macro should be mapped to the + * application-specific logging implementation that supports warning logging. + * + * @note This logging macro is called in the SNTP library with parameters wrapped in + * double parentheses to be ISO C89/C90 standard compliant. For a reference + * POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the + * logging-stack in demos folder of the + * [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C/). + * + * Default value: Warning logs are turned off, and no code is generated for calls + * to the macro in the SNTP library on compilation. + */ +#ifndef LogWarn + #define LogWarn( message ) +#endif + +/** + * @brief Macro that is called in the SNTP library for logging "Info" level + * messages. + * + * To enable info level logging in the SNTP library, this macro should be mapped to the + * application-specific logging implementation that supports info logging. + * + * @note This logging macro is called in the SNTP library with parameters wrapped in + * double parentheses to be ISO C89/C90 standard compliant. For a reference + * POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the + * logging-stack in demos folder of the + * [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C/). + * + * Default value: Info logging is turned off, and no code is generated for calls + * to the macro in the SNTP library on compilation. + */ +#ifndef LogInfo + #define LogInfo( message ) +#endif + +/** + * @brief Macro that is called in the SNTP library for logging "Debug" level + * messages. + * + * To enable debug level logging from SNTP library, this macro should be mapped to the + * application-specific logging implementation that supports debug logging. + * + * @note This logging macro is called in the SNTP library with parameters wrapped in + * double parentheses to be ISO C89/C90 standard compliant. For a reference + * POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the + * logging-stack in demos folder of the + * [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C/). + * + * Default value: Debug logging is turned off, and no code is generated for calls + * to the macro in the SNTP library on compilation. + */ +#ifndef LogDebug + #define LogDebug( message ) +#endif + +#endif /* ifndef CORE_SNTP_CONFIG_DEFAULTS_H_ */ diff --git a/test/cbmc/include/core_sntp_stubs.h b/test/cbmc/include/core_sntp_stubs.h new file mode 100644 index 0000000..4054852 --- /dev/null +++ b/test/cbmc/include/core_sntp_stubs.h @@ -0,0 +1,137 @@ +/* + * 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_stubs_stubs.h + * @brief Stubs definitions to generate client authentication codes and validate server authentication. + */ +#ifndef CORE_SNTP_STUBS_H_ +#define CORE_SNTP_STUBS_H_ + +#include +#include +#include +#include "core_sntp_client.h" + +/** + * @brief Application defined network interface send function. + * + * @param[in] pNetworkContext Application defined network interface context. + * @param[in] serverAddr Server address to which application sends data. + * @param[in] serverPort Server port to which application sends data. + * @param[out] pBuffer SNTP network send buffer. + * @param[in] bytesToSend Number of bytes to send over the network. + * + * @return Any value from INT32_MIN to INT32_MAX. + */ +int32_t NetworkInterfaceSendStub( NetworkContext_t * pNetworkContext, + uint32_t serverAddr, + uint16_t serverPort, + const void * pBuffer, + size_t bytesToSend ); + +/** + * @brief Application defined network interface receive function. + * + * @param[in] pNetworkContext Application defined network interface context. + * @param[in] serverAddr Server address from which application receives data. + * @param[in] serverPort Server port from which application receives data. + * @param[out] pBuffer SNTP network receive buffer. + * @param[in] bytesToRecv SNTP requested bytes. + * + * @return Any value from INT32_MIN to INT32_MAX. + */ +int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext, + uint32_t serverAddr, + uint16_t serverPort, + void * pBuffer, + size_t bytesToRecv ); + +/** + * @brief Application defined function to generate and append + * authentication code in an SNTP request buffer for the SNTP client to be + * authenticated by the time server, if a security mechanism is used. + * + * @param[in] pContext Application defined authentication interface context. + * @param[in] pTimeServer The time server being used to request time from. + * This parameter is useful to choose the security mechanism when multiple time + * servers are configured in the library, and they require different security + * mechanisms or authentication credentials to use. + * @param[in] pBuffer SNTP request buffer. + * @param[in] bufferSize The maximum amount of data that can be held by the buffer. + * @param[out] pAuthCodeSize This should be filled with size of the authentication + * data appended to the SNTP request buffer, @p pBuffer. + * + * @return The function SHOULD return one of the following integer codes: + * - #SntpSuccess when the authentication data is successfully appended to @p pBuffer. + * - #SntpErrorBufferTooSmall when the user-supplied buffer (to the SntpContext_t through + * @ref Sntp_Init) is not large enough to hold authentication data. + */ +SntpStatus_t GenerateClientAuthStub( SntpAuthContext_t * pContext, + const SntpServerInfo_t * pTimeServer, + void * pBuffer, + size_t bufferSize, + size_t * pAuthCodeSize ); + +/** + * @brief Application defined function to resolve time server domain-name + * to an IPv4 address. + * + * @param[in] pTimeServer The time-server whose IPv4 address is to be resolved. + * @param[out] pIpV4Addr This should be filled with the resolved IPv4 address. + * of @p pTimeServer. + * + * @return `true` if DNS resolution is successful; otherwise `false` to represent + * failure. + */ +bool ResolveDnsFuncStub( const SntpServerInfo_t * pServerAddr, + uint32_t * pIpV4Addr ); + +/** + * @brief Application defined function to obtain the current system time + * in SNTP timestamp format. + * + * @param[out] pCurrentTime This should be filled with the current system time + * in SNTP timestamp format. + * + * @return `true` if obtaining system time is successful; otherwise `false` to + * represent failure. + */ +bool GetTimeFuncStub( SntpTimestamp_t * pCurrentTime ); + +/** + * @brief Application defined function to update the system clock time + * so that it is synchronized the time server used for getting current time. + * + * @param[in] pTimeServer The time server used to request time. + * @param[in] pServerTime The current time returned by the @p pTimeServer. + * @param[in] clockOffSetSec The calculated clock offset of the system relative + * to the server time. + * + * @return `true` if setting system time is successful; otherwise `false` to + * represent failure. + */ +bool SetTimeFuncStub( const SntpServerInfo_t * pTimeServer, + const SntpTimestamp_t * pServerTime, + int32_t clockOffsetSec ); + +#endif /* ifndef CORE_SNTP_STUBS_H_ */ diff --git a/test/cbmc/sources/core_sntp_cbmc_state.c b/test/cbmc/sources/core_sntp_cbmc_state.c new file mode 100644 index 0000000..f0180c4 --- /dev/null +++ b/test/cbmc/sources/core_sntp_cbmc_state.c @@ -0,0 +1,113 @@ +/* + * 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.c + * @brief Implements the functions defined in core_sntp_cbmc_state.h. + */ +#include +#include +#include "core_sntp_client.h" +#include "core_sntp_cbmc_state.h" +#include "core_sntp_stubs.h" + +SntpContext_t * allocateCoreSntpContext( SntpContext_t * pContext ) +{ + SntpServerInfo_t * pTimeServers; + size_t currentServerIndex; + size_t numOfServers; + uint8_t * pNetworkBuffer; + size_t bufferSize; + SntpResolveDns_t resolveDnsFunc; + SntpGetTime_t getTimeFunc; + SntpSetTime_t setTimeFunc; + UdpTransportInterface_t * pNetworkIntf; + SntpAuthenticationInterface_t * pAuthIntf; + SntpStatus_t sntpStatus = SntpSuccess; + + if( pContext == NULL ) + { + pContext = malloc( sizeof( SntpContext_t ) ); + } + + __CPROVER_assume( numOfServers < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( currentServerIndex < CBMC_MAX_OBJECT_SIZE ); + + if( numOfServers == 0 ) + { + pTimeServers = NULL; + } + else + { + pTimeServers = malloc( numOfServers * sizeof( SntpServerInfo_t ) ); + } + + if( pTimeServers != NULL ) + { + __CPROVER_assume( pTimeServers->serverNameLen < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( pTimeServers->port < CBMC_MAX_OBJECT_SIZE ); + pTimeServers->pServerName = malloc( pTimeServers->serverNameLen ); + } + + __CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE ); + pNetworkBuffer = malloc( bufferSize ); + + pNetworkIntf = malloc( sizeof( UdpTransportInterface_t ) ); + + if( pNetworkIntf != NULL ) + { + pNetworkIntf->pUserContext = malloc( sizeof( NetworkContext_t ) ); + pNetworkIntf->sendTo = NetworkInterfaceSendStub; + pNetworkIntf->recvFrom = NetworkInterfaceReceiveStub; + } + + pAuthIntf = malloc( sizeof( SntpAuthenticationInterface_t ) ); + + if( pAuthIntf != NULL ) + { + pAuthIntf->pAuthContext = malloc( sizeof( SntpAuthContext_t ) ); + pAuthIntf->generateClientAuth = GenerateClientAuthStub; + } + + /* It is part of the API contract to call Sntp_Init() with the SntpContext_t + * before any other function in core_sntp_client.h. */ + if( pContext != NULL ) + { + resolveDnsFunc = ResolveDnsFuncStub; + getTimeFunc = GetTimeFuncStub; + setTimeFunc = SetTimeFuncStub; + pContext->currentServerIndex = currentServerIndex; + sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, pNetworkBuffer, + bufferSize, resolveDnsFunc, getTimeFunc, setTimeFunc, + pNetworkIntf, pAuthIntf ); + } + + /* If the SntpContext_t initialization failed, then set the context to NULL + * so that function under harness will return immediately upon a NULL + * parameter check. */ + if( sntpStatus != SntpSuccess ) + { + pContext = NULL; + } + + return pContext; +} diff --git a/test/cbmc/stubs/core_sntp_stubs.c b/test/cbmc/stubs/core_sntp_stubs.c new file mode 100644 index 0000000..b3e0a96 --- /dev/null +++ b/test/cbmc/stubs/core_sntp_stubs.c @@ -0,0 +1,183 @@ +/* + * 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_stubs.c + * @brief Stubs to generate client authentication codes and validate server authentication. + */ + +#include +#include "core_sntp_client.h" +#include "core_sntp_serializer.h" +#include "core_sntp_stubs.h" + +#define TEST_TIMESTAMP \ + { \ + .seconds = UINT32_MAX, \ + .fractions = 1000 \ + } + +/* An exclusive bound on the times that the NetworkInterfaceSendStub will be + * invoked before returning a loop terminating value. This is usually defined + * in the Makefile of the harnessed function. */ +#ifndef MAX_NETWORK_SEND_TRIES + #define MAX_NETWORK_SEND_TRIES 3 +#endif + +/* An exclusive bound on the times that the NetworkInterfaceReceiveStub will + * return an unbound value. At this value and beyond, the + * NetworkInterfaceReceiveStub will return zero on every call. */ +#ifndef MAX_NETWORK_RECV_TRIES + #define MAX_NETWORK_RECV_TRIES 4 +#endif + +static SntpTimestamp_t testTime = TEST_TIMESTAMP; + +int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext, + uint32_t serverAddr, + uint16_t serverPort, + void * pBuffer, + size_t bytesToRecv ) +{ + __CPROVER_assert( pBuffer != NULL, + "NetworkInterfaceReceiveStub pBuffer is NULL." ); + + __CPROVER_assert( __CPROVER_w_ok( pBuffer, bytesToRecv ), + "NetworkInterfaceReceiveStub pBuffer is writable up to bytesToRecv." ); + + __CPROVER_havoc_object( pBuffer ); + + int32_t bytesOrError; + static size_t tries = 0; + + /* It is a bug for the application defined transport send function to return + * more than bytesToRecv. */ + __CPROVER_assume( bytesOrError <= ( int32_t ) bytesToRecv ); + + if( tries < ( MAX_NETWORK_RECV_TRIES - 1 ) ) + { + tries++; + } + else + { + bytesOrError = 0; + } + + return bytesOrError; +} +int32_t NetworkInterfaceSendStub( NetworkContext_t * pNetworkContext, + uint32_t serverAddr, + uint16_t serverPort, + const void * pBuffer, + size_t bytesToSend ) +{ + __CPROVER_assert( pBuffer != NULL, + "NetworkInterfaceSendStub pBuffer is NULL." ); + + /* The number of tries to send the message before this invocation. */ + static size_t tries = 1; + + int32_t bytesOrError; + + /* It is a bug for the application defined transport send function to return + * more than bytesToSend. */ + __CPROVER_assume( bytesOrError <= ( int32_t ) bytesToSend ); + + /* If the maximum tries are reached, then return a timeout. In the SNTP library + * this stub is wrapped in a loop that will does not end until the bytesOrError + * returned is negative. This means we could loop possibly INT32_MAX + * iterations. Looping for INT32_MAX times adds no value to the proof. + * What matters is that the SNTP library can handle all the possible values + * that could be returned. */ + if( tries < ( MAX_NETWORK_SEND_TRIES - 1 ) ) + { + tries++; + } + else + { + tries = 1; + bytesOrError = bytesToSend; + } + + return bytesOrError; +} + +SntpStatus_t GenerateClientAuthStub( SntpAuthContext_t * pContext, + const SntpServerInfo_t * pTimeServer, + void * pBuffer, + size_t bufferSize, + size_t * pAuthCodeSize ) +{ + SntpStatus_t sntpStatus = SntpSuccess; + + if( bufferSize <= SNTP_PACKET_BASE_SIZE ) + { + sntpStatus = SntpErrorBufferTooSmall; + } + else + { + *pAuthCodeSize = SNTP_PACKET_BASE_SIZE; + } + + return sntpStatus; +} + +bool ResolveDnsFuncStub( const SntpServerInfo_t * pServerAddr, + uint32_t * pIpV4Addr ) +{ + /* For the proofs, returning a non deterministic boolean value + * will be good enough. */ + return nondet_bool(); +} + +bool GetTimeFuncStub( SntpTimestamp_t * pCurrentTime ) +{ + bool value = nondet_bool(); + + if( value ) + { + testTime.fractions = testTime.fractions + ( uint32_t ) 100000000; + } + else + { + testTime.fractions = testTime.fractions - ( uint32_t ) 1; + } + + *pCurrentTime = testTime; + + return value; +} + +bool SetTimeFuncStub( const SntpServerInfo_t * pTimeServer, + const SntpTimestamp_t * pServerTime, + int32_t clockOffsetSec ) +{ + return nondet_bool(); +} + +SntpStatus_t Sntp_SerializeRequest( SntpTimestamp_t * pRequestTime, + uint32_t randomNumber, + void * pBuffer, + size_t bufferSize ) +{ + return SntpSuccess; +} From 439b68ceabb60d1d927f7df44859de6b0a6bb612 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 13 May 2021 18:39:52 -0700 Subject: [PATCH 37/44] UPdating Lexicon.txt --- lexicon.txt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lexicon.txt b/lexicon.txt index 62338fa..a4341c9 100644 --- a/lexicon.txt +++ b/lexicon.txt @@ -10,12 +10,14 @@ backoff beforelooptime br buffersize +bytesorerror bytesremaining bytessent bytestorecv bytestorecv bytestosend bytestosend +cbmc clienttxtime clockfreqtolerance clockoffsetsec @@ -68,6 +70,7 @@ kod leapversionmode lsb misra +networkinterfacereceivestub nist noleapsecond noninfringement From 76a938a8911a00604bce85c05f0349582eeffb5a Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 13 May 2021 18:41:42 -0700 Subject: [PATCH 38/44] UPdating Lexicon.txt --- lexicon.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/lexicon.txt b/lexicon.txt index a4341c9..89b4040 100644 --- a/lexicon.txt +++ b/lexicon.txt @@ -71,6 +71,7 @@ leapversionmode lsb misra networkinterfacereceivestub +networkinterfacesendstub nist noleapsecond noninfringement From 020d59f8e5e607458aad203fde7dfaa588117b9d Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 13 May 2021 18:35:21 -0700 Subject: [PATCH 39/44] Sntp_SendTimeRequest proof --- test/cbmc/include/core_sntp_cbmc_state.h | 53 +++++++ test/cbmc/include/core_sntp_config.h | 175 ++++++++++++++++++++++ test/cbmc/include/core_sntp_stubs.h | 137 +++++++++++++++++ test/cbmc/sources/core_sntp_cbmc_state.c | 113 ++++++++++++++ test/cbmc/stubs/core_sntp_stubs.c | 183 +++++++++++++++++++++++ 5 files changed, 661 insertions(+) create mode 100644 test/cbmc/include/core_sntp_cbmc_state.h create mode 100644 test/cbmc/include/core_sntp_config.h create mode 100644 test/cbmc/include/core_sntp_stubs.h create mode 100644 test/cbmc/sources/core_sntp_cbmc_state.c create mode 100644 test/cbmc/stubs/core_sntp_stubs.c diff --git a/test/cbmc/include/core_sntp_cbmc_state.h b/test/cbmc/include/core_sntp_cbmc_state.h new file mode 100644 index 0000000..64900bf --- /dev/null +++ b/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_ */ diff --git a/test/cbmc/include/core_sntp_config.h b/test/cbmc/include/core_sntp_config.h new file mode 100644 index 0000000..2ee1a39 --- /dev/null +++ b/test/cbmc/include/core_sntp_config.h @@ -0,0 +1,175 @@ +/* + * coreSNTP v1.0.0 + * Copyright (C) 2020 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_config_defaults.h + * @brief This file represents the default values for the configuration macros + * of the coreSNTP library. + * + * @note This file SHOULD NOT be modified. If custom values are needed for + * any configuration macro, a core_sntp_config.h file should be provided to + * the SNTP library to override the default values defined in this file. + * To build the library with the core_sntp_config.h file, make sure to + * not set the SNTP_DO_NOT_USE_CUSTOM_CONFIG preprocessor macro. + */ + +#ifndef CORE_SNTP_CONFIG_DEFAULTS_H_ +#define CORE_SNTP_CONFIG_DEFAULTS_H_ + +/* The macro definition for SNTP_DO_NOT_USE_CUSTOM_CONFIG is for Doxygen + * documentation only. */ + +/** + * @brief Define this macro to build the SNTP library without the custom config + * file core_sntp_config.h. + * + * Without the custom config, the SNTP library builds with + * default values of config macros defined in core_sntp_config_defaults.h file. + * + * If a custom config is provided, then SNTP_DO_NOT_USE_CUSTOM_CONFIG should not + * be defined. + */ +#ifdef DOXYGEN + #define SNTP_DO_NOT_USE_CUSTOM_CONFIG +#endif + +/** + * @brief The maximum duration between non-empty network reads while + * receiving an SNTP packet via the #Sntp_ReceiveTimeResponse API function. + * + * When an incoming SNTP packet is detected, the transport receive function + * may be called multiple times until all of the expected number of bytes of the + * packet are received. This timeout represents the maximum polling duration that + * is allowed without any data reception from the network for the incoming packet. + * + * If the timeout expires, the #Sntp_ReceiveTimeResponse function will return + * #SntpErrorNetworkFailure. + * + * Possible values: Any positive 16 bit integer. Recommended to use a + * small timeout value.
+ * Default value: `10` + */ +#ifndef SNTP_RECV_POLLING_TIMEOUT_MS + #define SNTP_RECV_POLLING_TIMEOUT_MS ( 10U ) +#endif + +/** + * @brief The maximum duration between non-empty network transmissions while + * sending an SNTP packet via the #Sntp_SendTimeRequest API function. + * + * When sending an SNTP packet, the transport send function may be called multiple + * times until all of the required number of bytes are sent. + * This timeout represents the maximum duration that is allowed for no data + * transmission over the network through the transport send function. + * + * If the timeout expires, the #Sntp_SendTimeRequest function will return + * #SntpErrorNetworkFailure. + * + * Possible values: Any positive 16 bit integer. Recommended to use a small + * timeout value.
+ * Default value: `10` + */ +#ifndef SNTP_SEND_RETRY_TIMEOUT_MS + #define SNTP_SEND_RETRY_TIMEOUT_MS ( 10U ) +#endif + +/** + * @brief Macro that is called in the SNTP library for logging "Error" level + * messages. + * + * To enable error level logging in the SNTP library, this macro should be mapped to the + * application-specific logging implementation that supports error logging. + * + * @note This logging macro is called in the SNTP library with parameters wrapped in + * double parentheses to be ISO C89/C90 standard compliant. For a reference + * POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the + * logging-stack in demos folder of the + * [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C). + * + * Default value: Error logging is turned off, and no code is generated for calls + * to the macro in the SNTP library on compilation. + */ +#ifndef LogError + #define LogError( message ) +#endif + +/** + * @brief Macro that is called in the SNTP library for logging "Warning" level + * messages. + * + * To enable warning level logging in the SNTP library, this macro should be mapped to the + * application-specific logging implementation that supports warning logging. + * + * @note This logging macro is called in the SNTP library with parameters wrapped in + * double parentheses to be ISO C89/C90 standard compliant. For a reference + * POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the + * logging-stack in demos folder of the + * [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C/). + * + * Default value: Warning logs are turned off, and no code is generated for calls + * to the macro in the SNTP library on compilation. + */ +#ifndef LogWarn + #define LogWarn( message ) +#endif + +/** + * @brief Macro that is called in the SNTP library for logging "Info" level + * messages. + * + * To enable info level logging in the SNTP library, this macro should be mapped to the + * application-specific logging implementation that supports info logging. + * + * @note This logging macro is called in the SNTP library with parameters wrapped in + * double parentheses to be ISO C89/C90 standard compliant. For a reference + * POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the + * logging-stack in demos folder of the + * [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C/). + * + * Default value: Info logging is turned off, and no code is generated for calls + * to the macro in the SNTP library on compilation. + */ +#ifndef LogInfo + #define LogInfo( message ) +#endif + +/** + * @brief Macro that is called in the SNTP library for logging "Debug" level + * messages. + * + * To enable debug level logging from SNTP library, this macro should be mapped to the + * application-specific logging implementation that supports debug logging. + * + * @note This logging macro is called in the SNTP library with parameters wrapped in + * double parentheses to be ISO C89/C90 standard compliant. For a reference + * POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the + * logging-stack in demos folder of the + * [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C/). + * + * Default value: Debug logging is turned off, and no code is generated for calls + * to the macro in the SNTP library on compilation. + */ +#ifndef LogDebug + #define LogDebug( message ) +#endif + +#endif /* ifndef CORE_SNTP_CONFIG_DEFAULTS_H_ */ diff --git a/test/cbmc/include/core_sntp_stubs.h b/test/cbmc/include/core_sntp_stubs.h new file mode 100644 index 0000000..4054852 --- /dev/null +++ b/test/cbmc/include/core_sntp_stubs.h @@ -0,0 +1,137 @@ +/* + * 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_stubs_stubs.h + * @brief Stubs definitions to generate client authentication codes and validate server authentication. + */ +#ifndef CORE_SNTP_STUBS_H_ +#define CORE_SNTP_STUBS_H_ + +#include +#include +#include +#include "core_sntp_client.h" + +/** + * @brief Application defined network interface send function. + * + * @param[in] pNetworkContext Application defined network interface context. + * @param[in] serverAddr Server address to which application sends data. + * @param[in] serverPort Server port to which application sends data. + * @param[out] pBuffer SNTP network send buffer. + * @param[in] bytesToSend Number of bytes to send over the network. + * + * @return Any value from INT32_MIN to INT32_MAX. + */ +int32_t NetworkInterfaceSendStub( NetworkContext_t * pNetworkContext, + uint32_t serverAddr, + uint16_t serverPort, + const void * pBuffer, + size_t bytesToSend ); + +/** + * @brief Application defined network interface receive function. + * + * @param[in] pNetworkContext Application defined network interface context. + * @param[in] serverAddr Server address from which application receives data. + * @param[in] serverPort Server port from which application receives data. + * @param[out] pBuffer SNTP network receive buffer. + * @param[in] bytesToRecv SNTP requested bytes. + * + * @return Any value from INT32_MIN to INT32_MAX. + */ +int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext, + uint32_t serverAddr, + uint16_t serverPort, + void * pBuffer, + size_t bytesToRecv ); + +/** + * @brief Application defined function to generate and append + * authentication code in an SNTP request buffer for the SNTP client to be + * authenticated by the time server, if a security mechanism is used. + * + * @param[in] pContext Application defined authentication interface context. + * @param[in] pTimeServer The time server being used to request time from. + * This parameter is useful to choose the security mechanism when multiple time + * servers are configured in the library, and they require different security + * mechanisms or authentication credentials to use. + * @param[in] pBuffer SNTP request buffer. + * @param[in] bufferSize The maximum amount of data that can be held by the buffer. + * @param[out] pAuthCodeSize This should be filled with size of the authentication + * data appended to the SNTP request buffer, @p pBuffer. + * + * @return The function SHOULD return one of the following integer codes: + * - #SntpSuccess when the authentication data is successfully appended to @p pBuffer. + * - #SntpErrorBufferTooSmall when the user-supplied buffer (to the SntpContext_t through + * @ref Sntp_Init) is not large enough to hold authentication data. + */ +SntpStatus_t GenerateClientAuthStub( SntpAuthContext_t * pContext, + const SntpServerInfo_t * pTimeServer, + void * pBuffer, + size_t bufferSize, + size_t * pAuthCodeSize ); + +/** + * @brief Application defined function to resolve time server domain-name + * to an IPv4 address. + * + * @param[in] pTimeServer The time-server whose IPv4 address is to be resolved. + * @param[out] pIpV4Addr This should be filled with the resolved IPv4 address. + * of @p pTimeServer. + * + * @return `true` if DNS resolution is successful; otherwise `false` to represent + * failure. + */ +bool ResolveDnsFuncStub( const SntpServerInfo_t * pServerAddr, + uint32_t * pIpV4Addr ); + +/** + * @brief Application defined function to obtain the current system time + * in SNTP timestamp format. + * + * @param[out] pCurrentTime This should be filled with the current system time + * in SNTP timestamp format. + * + * @return `true` if obtaining system time is successful; otherwise `false` to + * represent failure. + */ +bool GetTimeFuncStub( SntpTimestamp_t * pCurrentTime ); + +/** + * @brief Application defined function to update the system clock time + * so that it is synchronized the time server used for getting current time. + * + * @param[in] pTimeServer The time server used to request time. + * @param[in] pServerTime The current time returned by the @p pTimeServer. + * @param[in] clockOffSetSec The calculated clock offset of the system relative + * to the server time. + * + * @return `true` if setting system time is successful; otherwise `false` to + * represent failure. + */ +bool SetTimeFuncStub( const SntpServerInfo_t * pTimeServer, + const SntpTimestamp_t * pServerTime, + int32_t clockOffsetSec ); + +#endif /* ifndef CORE_SNTP_STUBS_H_ */ diff --git a/test/cbmc/sources/core_sntp_cbmc_state.c b/test/cbmc/sources/core_sntp_cbmc_state.c new file mode 100644 index 0000000..f0180c4 --- /dev/null +++ b/test/cbmc/sources/core_sntp_cbmc_state.c @@ -0,0 +1,113 @@ +/* + * 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.c + * @brief Implements the functions defined in core_sntp_cbmc_state.h. + */ +#include +#include +#include "core_sntp_client.h" +#include "core_sntp_cbmc_state.h" +#include "core_sntp_stubs.h" + +SntpContext_t * allocateCoreSntpContext( SntpContext_t * pContext ) +{ + SntpServerInfo_t * pTimeServers; + size_t currentServerIndex; + size_t numOfServers; + uint8_t * pNetworkBuffer; + size_t bufferSize; + SntpResolveDns_t resolveDnsFunc; + SntpGetTime_t getTimeFunc; + SntpSetTime_t setTimeFunc; + UdpTransportInterface_t * pNetworkIntf; + SntpAuthenticationInterface_t * pAuthIntf; + SntpStatus_t sntpStatus = SntpSuccess; + + if( pContext == NULL ) + { + pContext = malloc( sizeof( SntpContext_t ) ); + } + + __CPROVER_assume( numOfServers < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( currentServerIndex < CBMC_MAX_OBJECT_SIZE ); + + if( numOfServers == 0 ) + { + pTimeServers = NULL; + } + else + { + pTimeServers = malloc( numOfServers * sizeof( SntpServerInfo_t ) ); + } + + if( pTimeServers != NULL ) + { + __CPROVER_assume( pTimeServers->serverNameLen < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( pTimeServers->port < CBMC_MAX_OBJECT_SIZE ); + pTimeServers->pServerName = malloc( pTimeServers->serverNameLen ); + } + + __CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE ); + pNetworkBuffer = malloc( bufferSize ); + + pNetworkIntf = malloc( sizeof( UdpTransportInterface_t ) ); + + if( pNetworkIntf != NULL ) + { + pNetworkIntf->pUserContext = malloc( sizeof( NetworkContext_t ) ); + pNetworkIntf->sendTo = NetworkInterfaceSendStub; + pNetworkIntf->recvFrom = NetworkInterfaceReceiveStub; + } + + pAuthIntf = malloc( sizeof( SntpAuthenticationInterface_t ) ); + + if( pAuthIntf != NULL ) + { + pAuthIntf->pAuthContext = malloc( sizeof( SntpAuthContext_t ) ); + pAuthIntf->generateClientAuth = GenerateClientAuthStub; + } + + /* It is part of the API contract to call Sntp_Init() with the SntpContext_t + * before any other function in core_sntp_client.h. */ + if( pContext != NULL ) + { + resolveDnsFunc = ResolveDnsFuncStub; + getTimeFunc = GetTimeFuncStub; + setTimeFunc = SetTimeFuncStub; + pContext->currentServerIndex = currentServerIndex; + sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, pNetworkBuffer, + bufferSize, resolveDnsFunc, getTimeFunc, setTimeFunc, + pNetworkIntf, pAuthIntf ); + } + + /* If the SntpContext_t initialization failed, then set the context to NULL + * so that function under harness will return immediately upon a NULL + * parameter check. */ + if( sntpStatus != SntpSuccess ) + { + pContext = NULL; + } + + return pContext; +} diff --git a/test/cbmc/stubs/core_sntp_stubs.c b/test/cbmc/stubs/core_sntp_stubs.c new file mode 100644 index 0000000..b3e0a96 --- /dev/null +++ b/test/cbmc/stubs/core_sntp_stubs.c @@ -0,0 +1,183 @@ +/* + * 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_stubs.c + * @brief Stubs to generate client authentication codes and validate server authentication. + */ + +#include +#include "core_sntp_client.h" +#include "core_sntp_serializer.h" +#include "core_sntp_stubs.h" + +#define TEST_TIMESTAMP \ + { \ + .seconds = UINT32_MAX, \ + .fractions = 1000 \ + } + +/* An exclusive bound on the times that the NetworkInterfaceSendStub will be + * invoked before returning a loop terminating value. This is usually defined + * in the Makefile of the harnessed function. */ +#ifndef MAX_NETWORK_SEND_TRIES + #define MAX_NETWORK_SEND_TRIES 3 +#endif + +/* An exclusive bound on the times that the NetworkInterfaceReceiveStub will + * return an unbound value. At this value and beyond, the + * NetworkInterfaceReceiveStub will return zero on every call. */ +#ifndef MAX_NETWORK_RECV_TRIES + #define MAX_NETWORK_RECV_TRIES 4 +#endif + +static SntpTimestamp_t testTime = TEST_TIMESTAMP; + +int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext, + uint32_t serverAddr, + uint16_t serverPort, + void * pBuffer, + size_t bytesToRecv ) +{ + __CPROVER_assert( pBuffer != NULL, + "NetworkInterfaceReceiveStub pBuffer is NULL." ); + + __CPROVER_assert( __CPROVER_w_ok( pBuffer, bytesToRecv ), + "NetworkInterfaceReceiveStub pBuffer is writable up to bytesToRecv." ); + + __CPROVER_havoc_object( pBuffer ); + + int32_t bytesOrError; + static size_t tries = 0; + + /* It is a bug for the application defined transport send function to return + * more than bytesToRecv. */ + __CPROVER_assume( bytesOrError <= ( int32_t ) bytesToRecv ); + + if( tries < ( MAX_NETWORK_RECV_TRIES - 1 ) ) + { + tries++; + } + else + { + bytesOrError = 0; + } + + return bytesOrError; +} +int32_t NetworkInterfaceSendStub( NetworkContext_t * pNetworkContext, + uint32_t serverAddr, + uint16_t serverPort, + const void * pBuffer, + size_t bytesToSend ) +{ + __CPROVER_assert( pBuffer != NULL, + "NetworkInterfaceSendStub pBuffer is NULL." ); + + /* The number of tries to send the message before this invocation. */ + static size_t tries = 1; + + int32_t bytesOrError; + + /* It is a bug for the application defined transport send function to return + * more than bytesToSend. */ + __CPROVER_assume( bytesOrError <= ( int32_t ) bytesToSend ); + + /* If the maximum tries are reached, then return a timeout. In the SNTP library + * this stub is wrapped in a loop that will does not end until the bytesOrError + * returned is negative. This means we could loop possibly INT32_MAX + * iterations. Looping for INT32_MAX times adds no value to the proof. + * What matters is that the SNTP library can handle all the possible values + * that could be returned. */ + if( tries < ( MAX_NETWORK_SEND_TRIES - 1 ) ) + { + tries++; + } + else + { + tries = 1; + bytesOrError = bytesToSend; + } + + return bytesOrError; +} + +SntpStatus_t GenerateClientAuthStub( SntpAuthContext_t * pContext, + const SntpServerInfo_t * pTimeServer, + void * pBuffer, + size_t bufferSize, + size_t * pAuthCodeSize ) +{ + SntpStatus_t sntpStatus = SntpSuccess; + + if( bufferSize <= SNTP_PACKET_BASE_SIZE ) + { + sntpStatus = SntpErrorBufferTooSmall; + } + else + { + *pAuthCodeSize = SNTP_PACKET_BASE_SIZE; + } + + return sntpStatus; +} + +bool ResolveDnsFuncStub( const SntpServerInfo_t * pServerAddr, + uint32_t * pIpV4Addr ) +{ + /* For the proofs, returning a non deterministic boolean value + * will be good enough. */ + return nondet_bool(); +} + +bool GetTimeFuncStub( SntpTimestamp_t * pCurrentTime ) +{ + bool value = nondet_bool(); + + if( value ) + { + testTime.fractions = testTime.fractions + ( uint32_t ) 100000000; + } + else + { + testTime.fractions = testTime.fractions - ( uint32_t ) 1; + } + + *pCurrentTime = testTime; + + return value; +} + +bool SetTimeFuncStub( const SntpServerInfo_t * pTimeServer, + const SntpTimestamp_t * pServerTime, + int32_t clockOffsetSec ) +{ + return nondet_bool(); +} + +SntpStatus_t Sntp_SerializeRequest( SntpTimestamp_t * pRequestTime, + uint32_t randomNumber, + void * pBuffer, + size_t bufferSize ) +{ + return SntpSuccess; +} From 8645138fce291f733688f731dd0c9ee98f385cf8 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 13 May 2021 18:39:52 -0700 Subject: [PATCH 40/44] UPdating Lexicon.txt --- lexicon.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lexicon.txt b/lexicon.txt index 932efbe..815163f 100644 --- a/lexicon.txt +++ b/lexicon.txt @@ -12,6 +12,7 @@ beforelooptime blocktimems br buffersize +bytesorerror bytesremaining bytessent bytestorecv @@ -19,7 +20,6 @@ bytestorecv bytestosend bytestosend cbmc -clienttime clienttxtime clockfreqtolerance clockoffsetsec @@ -77,6 +77,7 @@ leapsecondinfo leapversionmode lsb misra +networkinterfacereceivestub nist noleapsecond noninfringement From 4c0208bf727289cb4fa497b3ee82d3e19f39d2cc Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 13 May 2021 18:41:42 -0700 Subject: [PATCH 41/44] UPdating Lexicon.txt --- lexicon.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/lexicon.txt b/lexicon.txt index 815163f..b164a5a 100644 --- a/lexicon.txt +++ b/lexicon.txt @@ -78,6 +78,7 @@ leapversionmode lsb misra networkinterfacereceivestub +networkinterfacesendstub nist noleapsecond noninfringement From 7e6ffdd67d1fb698171c6c6e77b9b5f0d51f345e Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 13 May 2021 18:58:00 -0700 Subject: [PATCH 42/44] build fixes --- source/core_sntp_serializer.c | 3 --- 1 file changed, 3 deletions(-) diff --git a/source/core_sntp_serializer.c b/source/core_sntp_serializer.c index c2b343b..cef9272 100644 --- a/source/core_sntp_serializer.c +++ b/source/core_sntp_serializer.c @@ -32,8 +32,6 @@ /* Include API header. */ #include "core_sntp_serializer.h" -#pragma CPROVER check disable "unsigned-overflow" -#pragma CPROVER check disable "conversion" /** * @brief The version of SNTP supported by the coreSNTP library by complying @@ -404,7 +402,6 @@ static SntpStatus_t calculateClockOffset( const SntpTimestamp_t * pClientTxTime, status = SntpClockOffsetOverflow; } - #pragma CPROVER check pop return status; } From 3901b132a6154f3638d27714baf46ee563929583 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 13 May 2021 19:05:12 -0700 Subject: [PATCH 43/44] sntp_Init proof changes due to Sntp_init function chnanges --- test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c b/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c index 5351630..642cba9 100644 --- a/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c +++ b/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c @@ -40,6 +40,7 @@ void harness() SntpSetTime_t setSystemTimeFunc; UdpTransportInterface_t * pTransportIntf; SntpAuthenticationInterface_t * pAuthIntf; + uint32_t serverResponseTimeoutMs; SntpStatus_t sntpStatus; pContext = malloc( sizeof( SntpContext_t ) ); @@ -51,7 +52,7 @@ void harness() pTransportIntf = malloc( sizeof( UdpTransportInterface_t ) ); pAuthIntf = malloc( sizeof( SntpAuthenticationInterface_t ) ); - sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, pNetworkBuffer, + sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, serverResponseTimeoutMs, pNetworkBuffer, bufferSize, resolveDnsFunc, getSystemTimeFunc, setSystemTimeFunc, pTransportIntf, pAuthIntf ); From 76d873da3876e22042805d97b6b35e4dba11cfe1 Mon Sep 17 00:00:00 2001 From: Shivangi Gupta Date: Thu, 13 May 2021 19:08:45 -0700 Subject: [PATCH 44/44] Sntp_Init function changes applied to SendTimeRequest Proof --- test/cbmc/sources/core_sntp_cbmc_state.c | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/test/cbmc/sources/core_sntp_cbmc_state.c b/test/cbmc/sources/core_sntp_cbmc_state.c index f0180c4..b14ce07 100644 --- a/test/cbmc/sources/core_sntp_cbmc_state.c +++ b/test/cbmc/sources/core_sntp_cbmc_state.c @@ -35,6 +35,7 @@ SntpContext_t * allocateCoreSntpContext( SntpContext_t * pContext ) SntpServerInfo_t * pTimeServers; size_t currentServerIndex; size_t numOfServers; + uint32_t serverResponseTimeoutMs; uint8_t * pNetworkBuffer; size_t bufferSize; SntpResolveDns_t resolveDnsFunc; @@ -50,6 +51,7 @@ SntpContext_t * allocateCoreSntpContext( SntpContext_t * pContext ) } __CPROVER_assume( numOfServers < CBMC_MAX_OBJECT_SIZE ); + __CPROVER_assume( serverResponseTimeoutMs < CBMC_MAX_OBJECT_SIZE ); __CPROVER_assume( currentServerIndex < CBMC_MAX_OBJECT_SIZE ); if( numOfServers == 0 ) @@ -96,7 +98,7 @@ SntpContext_t * allocateCoreSntpContext( SntpContext_t * pContext ) getTimeFunc = GetTimeFuncStub; setTimeFunc = SetTimeFuncStub; pContext->currentServerIndex = currentServerIndex; - sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, pNetworkBuffer, + sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, serverResponseTimeoutMs, pNetworkBuffer, bufferSize, resolveDnsFunc, getTimeFunc, setTimeFunc, pNetworkIntf, pAuthIntf ); }