feat: add Jasmin assembly integration for crypto acceleration
- Integrated `zupt_mac_verify_ct` in `zupt_decrypt_buffer()` to replace C XOR loop for HMAC-SHA256 - Integrated `zupt_ct_select_32` in `zupt_mlkem768_decaps()` to replace C `cmov()` for FO transformation - Added `include/zupt_jasmin.h` with extern declarations and ABI docs - Added `#ifdef ZUPT_USE_JASMIN` guards with clean C fallbacks in `zupt_crypto.c` and `zupt_mlkem.c` - Makefile now auto-detects `jasmin/*.s`, assembles and links with `-DZUPT_USE_JASMIN` Closes #3
This commit is contained in:
Cristian Cezar Moisés
parent
cea317653e
commit
06c877ec86
43 changed files with 1913 additions and 546 deletions
|
|
@ -30,7 +30,7 @@
|
|||
#define zupt_mkdir(p) mkdir(p, 0755)
|
||||
#endif
|
||||
|
||||
#define ZUPT_VERSION_STRING "1.0.0"
|
||||
#define ZUPT_VERSION_STRING "1.5.0"
|
||||
#define ZUPT_FORMAT_MAJOR 1
|
||||
#define ZUPT_FORMAT_MINOR 4
|
||||
|
||||
|
|
|
|||
41
include/zupt_acsl.h
Normal file
41
include/zupt_acsl.h
Normal file
|
|
@ -0,0 +1,41 @@
|
|||
/*
|
||||
* Zupt — ACSL Custom Predicates for Frama-C/WP
|
||||
* Copyright (c) 2026 Cristian Cezar Moisés — MIT License
|
||||
*
|
||||
* 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 */
|
||||
28
include/zupt_cpuid.h
Normal file
28
include/zupt_cpuid.h
Normal file
|
|
@ -0,0 +1,28 @@
|
|||
/*
|
||||
* Zupt — CPU Feature Detection
|
||||
* Copyright (c) 2026 Cristian Cezar Moisés — MIT License
|
||||
*/
|
||||
#ifndef ZUPT_CPUID_H
|
||||
#define ZUPT_CPUID_H
|
||||
|
||||
#include <stdint.h>
|
||||
|
||||
typedef struct {
|
||||
int has_aesni; /* CPUID.01H:ECX[25] — AES-NI instructions */
|
||||
int has_pclmul; /* CPUID.01H:ECX[1] — CLMUL (carry-less multiply) */
|
||||
int has_avx2; /* CPUID.07H:EBX[5] — AVX2 (256-bit SIMD) */
|
||||
int has_sse41; /* CPUID.01H:ECX[19] — SSE4.1 */
|
||||
} zupt_cpu_features_t;
|
||||
|
||||
/*@ assigns f->has_aesni, f->has_pclmul, f->has_avx2, f->has_sse41;
|
||||
@ ensures f->has_aesni == 0 || f->has_aesni == 1;
|
||||
@ ensures f->has_pclmul == 0 || f->has_pclmul == 1;
|
||||
@ ensures f->has_avx2 == 0 || f->has_avx2 == 1;
|
||||
@ ensures f->has_sse41 == 0 || f->has_sse41 == 1;
|
||||
*/
|
||||
void zupt_detect_cpu(zupt_cpu_features_t *f);
|
||||
|
||||
/* Global instance — set once at program start */
|
||||
extern zupt_cpu_features_t zupt_cpu;
|
||||
|
||||
#endif /* ZUPT_CPUID_H */
|
||||
40
include/zupt_jasmin.h
Normal file
40
include/zupt_jasmin.h
Normal file
|
|
@ -0,0 +1,40 @@
|
|||
/*
|
||||
* Zupt — Jasmin Verified Crypto Declarations
|
||||
* Copyright (c) 2026 Cristian Cezar Moisés — MIT License
|
||||
*
|
||||
* Extern declarations for Jasmin-compiled assembly functions.
|
||||
* These replace C fallbacks when built with -DZUPT_USE_JASMIN.
|
||||
*
|
||||
* Calling convention: System V AMD64 ABI.
|
||||
* Pointer args passed in RDI, RSI, RDX, RCX, R8, R9.
|
||||
*/
|
||||
#ifndef ZUPT_JASMIN_H
|
||||
#define ZUPT_JASMIN_H
|
||||
|
||||
#ifdef ZUPT_USE_JASMIN
|
||||
#include <stdint.h>
|
||||
|
||||
/* JASMIN-VERIFIED: CT MAC comparison (4×u64 XOR accumulation).
|
||||
* Returns 0 if all 32 bytes match, nonzero if any differ.
|
||||
* Replaces XOR loop in zupt_decrypt_buffer(). */
|
||||
extern uint64_t zupt_mac_verify_ct(const void *expected, const void *actual);
|
||||
|
||||
/* JASMIN-VERIFIED: CT conditional select (4×u64 masked select).
|
||||
* if cond==0: copies a→out. if cond!=0: copies b→out.
|
||||
* Replaces cmov in zupt_mlkem768_decaps(). */
|
||||
extern void zupt_ct_select_32(void *out, const void *a,
|
||||
const void *b, uint64_t cond);
|
||||
|
||||
/* JASMIN-VERIFIED: CT conditional swap (4×u64 masked XOR swap).
|
||||
* if cond==0: no-op. if cond==1: swaps a↔b in place.
|
||||
* Replaces fe_cswap in zupt_x25519.c. */
|
||||
extern void zupt_fe_cswap(void *a, void *b, uint64_t cond);
|
||||
|
||||
/* NOTE: zupt_aes256_blk has an offset bug in the Jasmin-generated
|
||||
* assembly (stack u128[15] indexing uses byte offset instead of
|
||||
* element offset — rk.[1] generates [rsp+1] not [rsp+16]).
|
||||
* AES-NI path is NOT wired in until the .jazz source is fixed.
|
||||
* C table-based AES remains the active path. */
|
||||
|
||||
#endif /* ZUPT_USE_JASMIN */
|
||||
#endif /* ZUPT_JASMIN_H */
|
||||
49
include/zupt_keccak.h
Normal file
49
include/zupt_keccak.h
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
/*
|
||||
* Zupt — Backup-oriented compression with AES-256 encryption
|
||||
* Copyright (c) 2026 Cristian Cezar Moisés
|
||||
* SPDX-License-Identifier: MIT
|
||||
*
|
||||
* Keccak-f[1600] sponge: SHA3-256, SHA3-512, SHAKE-128, SHAKE-256
|
||||
* Required by ML-KEM-768 (FIPS 203).
|
||||
* Pure C11, zero dependencies, no dynamic allocation.
|
||||
*/
|
||||
#ifndef ZUPT_KECCAK_H
|
||||
#define ZUPT_KECCAK_H
|
||||
|
||||
#include <stdint.h>
|
||||
#include <stddef.h>
|
||||
|
||||
/* Sponge state: 25 × 64-bit lanes = 200 bytes */
|
||||
typedef struct {
|
||||
uint64_t st[25];
|
||||
uint8_t buf[200]; /* absorption buffer */
|
||||
size_t rate; /* rate in bytes */
|
||||
size_t pt; /* position in buf */
|
||||
uint8_t dsuf; /* domain suffix: 0x06 for SHA3, 0x1F for SHAKE */
|
||||
} zupt_keccak_ctx;
|
||||
|
||||
/* SHA3-256: 32-byte output */
|
||||
void zupt_sha3_256(const uint8_t *data, size_t len, uint8_t out[32]);
|
||||
|
||||
/* SHA3-512: 64-byte output */
|
||||
void zupt_sha3_512(const uint8_t *data, size_t len, uint8_t out[64]);
|
||||
|
||||
/* SHAKE-128: extendable output */
|
||||
void zupt_shake128(const uint8_t *data, size_t dlen, uint8_t *out, size_t olen);
|
||||
|
||||
/* SHAKE-256: extendable output */
|
||||
void zupt_shake256(const uint8_t *data, size_t dlen, uint8_t *out, size_t olen);
|
||||
|
||||
/* Incremental SHAKE-128 for ML-KEM sampling */
|
||||
void zupt_shake128_init(zupt_keccak_ctx *ctx);
|
||||
void zupt_shake128_absorb(zupt_keccak_ctx *ctx, const uint8_t *data, size_t len);
|
||||
void zupt_shake128_finalize(zupt_keccak_ctx *ctx);
|
||||
void zupt_shake128_squeeze(zupt_keccak_ctx *ctx, uint8_t *out, size_t len);
|
||||
|
||||
/* Incremental SHAKE-256 */
|
||||
void zupt_shake256_init(zupt_keccak_ctx *ctx);
|
||||
void zupt_shake256_absorb(zupt_keccak_ctx *ctx, const uint8_t *data, size_t len);
|
||||
void zupt_shake256_finalize(zupt_keccak_ctx *ctx);
|
||||
void zupt_shake256_squeeze(zupt_keccak_ctx *ctx, uint8_t *out, size_t len);
|
||||
|
||||
#endif
|
||||
65
include/zupt_mlkem.h
Normal file
65
include/zupt_mlkem.h
Normal file
|
|
@ -0,0 +1,65 @@
|
|||
/*
|
||||
* Zupt — Backup-oriented compression with AES-256 encryption
|
||||
* Copyright (c) 2026 Cristian Cezar Moisés
|
||||
* SPDX-License-Identifier: MIT
|
||||
*
|
||||
* ML-KEM-768 (FIPS 203, formerly CRYSTALS-Kyber).
|
||||
* Post-quantum key encapsulation mechanism.
|
||||
*
|
||||
* Parameters (ML-KEM-768):
|
||||
* k = 3, η₁ = 2, η₂ = 2, d_u = 10, d_v = 4
|
||||
* Public key: 1184 bytes
|
||||
* Secret key: 2400 bytes
|
||||
* Ciphertext: 1088 bytes
|
||||
* Shared secret: 32 bytes
|
||||
*
|
||||
* SECURITY NOTE: This implementation must undergo independent review
|
||||
* before deployment in high-assurance contexts. It targets correctness
|
||||
* against NIST test vectors and constant-time operation.
|
||||
*/
|
||||
#ifndef ZUPT_MLKEM_H
|
||||
#define ZUPT_MLKEM_H
|
||||
|
||||
#include <stdint.h>
|
||||
|
||||
#define MLKEM_K 3
|
||||
#define MLKEM_N 256
|
||||
#define MLKEM_Q 3329
|
||||
#define MLKEM_ETA1 2
|
||||
#define MLKEM_ETA2 2
|
||||
#define MLKEM_DU 10
|
||||
#define MLKEM_DV 4
|
||||
|
||||
#define MLKEM_PUBLICKEYBYTES 1184
|
||||
#define MLKEM_SECRETKEYBYTES 2400
|
||||
#define MLKEM_CIPHERTEXTBYTES 1088
|
||||
#define MLKEM_SSBYTES 32
|
||||
|
||||
/* KeyGen: generate public/secret keypair.
|
||||
* pk: output public key (1184 bytes)
|
||||
* sk: output secret key (2400 bytes)
|
||||
* Returns 0 on success. */
|
||||
int zupt_mlkem768_keygen(uint8_t pk[MLKEM_PUBLICKEYBYTES],
|
||||
uint8_t sk[MLKEM_SECRETKEYBYTES]);
|
||||
|
||||
/* Encapsulate: produce ciphertext and shared secret from public key.
|
||||
* ct: output ciphertext (1088 bytes)
|
||||
* ss: output shared secret (32 bytes)
|
||||
* pk: input public key (1184 bytes)
|
||||
* Returns 0 on success. */
|
||||
int zupt_mlkem768_encaps(uint8_t ct[MLKEM_CIPHERTEXTBYTES],
|
||||
uint8_t ss[MLKEM_SSBYTES],
|
||||
const uint8_t pk[MLKEM_PUBLICKEYBYTES]);
|
||||
|
||||
/* Decapsulate: recover shared secret from ciphertext and secret key.
|
||||
* ss: output shared secret (32 bytes)
|
||||
* ct: input ciphertext (1088 bytes)
|
||||
* sk: input secret key (2400 bytes)
|
||||
* Returns 0 on success.
|
||||
* CT-REQUIRED: Implicit rejection — invalid ciphertext produces a
|
||||
* pseudorandom shared secret (no distinguishable failure). */
|
||||
int zupt_mlkem768_decaps(uint8_t ss[MLKEM_SSBYTES],
|
||||
const uint8_t ct[MLKEM_CIPHERTEXTBYTES],
|
||||
const uint8_t sk[MLKEM_SECRETKEYBYTES]);
|
||||
|
||||
#endif
|
||||
22
include/zupt_x25519.h
Normal file
22
include/zupt_x25519.h
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
/*
|
||||
* Zupt — Backup-oriented compression with AES-256 encryption
|
||||
* Copyright (c) 2026 Cristian Cezar Moisés
|
||||
* SPDX-License-Identifier: MIT
|
||||
*
|
||||
* X25519 Diffie-Hellman key agreement (RFC 7748).
|
||||
* Montgomery ladder — constant-time by construction.
|
||||
*/
|
||||
#ifndef ZUPT_X25519_H
|
||||
#define ZUPT_X25519_H
|
||||
|
||||
#include <stdint.h>
|
||||
|
||||
/* X25519(scalar, point) → result. All inputs/outputs are 32 bytes.
|
||||
* CT-REQUIRED: Montgomery ladder is inherently constant-time. */
|
||||
void zupt_x25519(uint8_t out[32], const uint8_t scalar[32], const uint8_t point[32]);
|
||||
|
||||
/* X25519 with the standard basepoint (9).
|
||||
* Used for keygen: public = X25519(private, basepoint). */
|
||||
void zupt_x25519_base(uint8_t out[32], const uint8_t scalar[32]);
|
||||
|
||||
#endif
|
||||
Loading…
Reference in a new issue