Improve mbedtls_ct_memmove_left w.r.t. const-flow tests

Signed-off-by: Dave Rodgman <dave.rodgman@arm.com>
This commit is contained in:
Dave Rodgman 2023-07-28 16:13:52 +01:00
parent 8de3482507
commit fa5a4bbb02
2 changed files with 20 additions and 6 deletions

View File

@ -30,6 +30,8 @@
#include "mbedtls/error.h" #include "mbedtls/error.h"
#include "mbedtls/platform_util.h" #include "mbedtls/platform_util.h"
#include "../tests/include/test/constant_flow.h"
#include <string.h> #include <string.h>
#if defined(MBEDTLS_USE_PSA_CRYPTO) && defined(MBEDTLS_SSL_SOME_SUITES_USE_MAC) #if defined(MBEDTLS_USE_PSA_CRYPTO) && defined(MBEDTLS_SSL_SOME_SUITES_USE_MAC)
@ -127,6 +129,20 @@ int mbedtls_ct_memcmp(const void *a,
void mbedtls_ct_memmove_left(void *start, size_t total, size_t offset) void mbedtls_ct_memmove_left(void *start, size_t total, size_t offset)
{ {
/* In case of inlining, ensure that code generated is independent of the value of offset
* (e.g., if the compiler knows that offset == 0, it might be able to optimise this function
* to a no-op). */
size_t hidden_offset = mbedtls_ct_compiler_opaque(offset);
/* During this loop, j will take every value from [0..total) exactly once,
* regardless of the value of hidden_offset (it only changes the initial
* value for j).
*
* For this reason, when testing, it is safe to mark hidden_offset as non-secret.
* This prevents the const-flow checkers from generating a false-positive.
*/
TEST_CF_PUBLIC(&hidden_offset, sizeof(hidden_offset));
/* Iterate over the array, reading each byte once and writing each byte once. */ /* Iterate over the array, reading each byte once and writing each byte once. */
for (size_t i = 0; i < total; i++) { for (size_t i = 0; i < total; i++) {
/* Each iteration, read one byte, and write it to start[i]. /* Each iteration, read one byte, and write it to start[i].
@ -138,9 +154,8 @@ void mbedtls_ct_memmove_left(void *start, size_t total, size_t offset)
* If the source address is out of range, mask it to zero. * If the source address is out of range, mask it to zero.
*/ */
// The address that we will read from // The offset that we will read from (if in range)
// TODO: if offset is marked as secret, this upsets Memsan. size_t j = i + hidden_offset;
size_t j = i + offset;
// Is the address off the end of the array? // Is the address off the end of the array?
mbedtls_ct_condition_t not_dummy = mbedtls_ct_bool_lt(j, total); mbedtls_ct_condition_t not_dummy = mbedtls_ct_bool_lt(j, total);

View File

@ -329,11 +329,10 @@ void mbedtls_ct_memmove_left(int len, int offset)
buf_expected[i] = buf[i]; buf_expected[i] = buf[i];
} }
//Note: Marking o as secret causes false positives from Memsan TEST_CF_SECRET(&o, sizeof(o));
//TEST_CF_SECRET(&o, sizeof(o));
TEST_CF_SECRET(buf, l); TEST_CF_SECRET(buf, l);
mbedtls_ct_memmove_left(buf, l, o); mbedtls_ct_memmove_left(buf, l, o);
//TEST_CF_PUBLIC(&o, sizeof(o)); TEST_CF_PUBLIC(&o, sizeof(o));
TEST_CF_PUBLIC(buf, l); TEST_CF_PUBLIC(buf, l);
if (l > 0) { if (l > 0) {