42 lines
1.2 KiB
C
42 lines
1.2 KiB
C
/*
|
|
* Zupt — ACSL Custom Predicates for Frama-C/WP
|
|
* SPDX-License-Identifier: AGPL-3.0-or-later
|
|
* Copyright (c) 2026 Cristian Cezar Moisés — AGPL-3.0-or-later (commercial: sac@securityops.co)
|
|
*
|
|
* Usage: frama-c -wp -wp-rte -wp-model Typed+Cast
|
|
* -cpp-extra-args="-Iinclude -Isrc" src/zupt_crypto.c
|
|
*/
|
|
#ifndef ZUPT_ACSL_H
|
|
#define ZUPT_ACSL_H
|
|
|
|
#ifdef __FRAMAC__
|
|
#include <stdint.h>
|
|
|
|
/*@ predicate ValidBuffer{L}(uint8_t *p, size_t n) =
|
|
@ \valid_read(p + (0..n-1)) &&
|
|
@ \initialized(p + (0..n-1));
|
|
@
|
|
@ predicate ValidWriteBuffer{L}(uint8_t *p, size_t n) =
|
|
@ \valid(p + (0..n-1));
|
|
@
|
|
@ predicate Separated2(uint8_t *a, size_t an,
|
|
@ uint8_t *b, size_t bn) =
|
|
@ \separated(a + (0..an-1), b + (0..bn-1));
|
|
@
|
|
@ predicate KeyWiped{L}(uint8_t *k, size_t n) =
|
|
@ \forall integer i; 0 <= i < n ==> \at(k[i],L) == 0;
|
|
@
|
|
@ predicate ValidKey{L}(uint8_t *k, size_t n) =
|
|
@ ValidBuffer{L}(k, n) && n == 32;
|
|
@
|
|
@ predicate ConstantTimeCompare{L}(uint8_t *a, uint8_t *b,
|
|
@ size_t n) =
|
|
@ \forall integer i; 0 <= i < n ==>
|
|
@ \initialized(\at(a+i,L)) && \initialized(\at(b+i,L));
|
|
@
|
|
@ predicate MACValid{L}(uint8_t *mac) =
|
|
@ ValidBuffer{L}(mac, 32);
|
|
*/
|
|
#endif /* __FRAMAC__ */
|
|
|
|
#endif /* ZUPT_ACSL_H */
|