keleusma 0.2.2

Total Functional Stream Processor with definitive WCET and WCMU verification, targeting no_std + alloc embedded scripting
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

#![cfg(feature = "verify")]

use keleusma::Arena;
use keleusma::bytecode::{
    BlockType, Chunk, Module, Op, RUNTIME_ADDRESS_BITS_LOG2, RUNTIME_FLOAT_BITS_LOG2,
    RUNTIME_WORD_BITS_LOG2,
};
use keleusma::vm::{DEFAULT_ARENA_CAPACITY, Vm, VmError};

fn make_chunk(name: &str, ops: Vec<Op>) -> Chunk {
    Chunk {
        name: String::from(name),
        ops,
        constants: Vec::new(),
        struct_templates: Vec::new(),
        local_count: 0,
        param_count: 0,
        block_type: BlockType::Func,
        param_types: Vec::new(),
        debug_pool: None,
    }
}

fn make_module(chunks: Vec<Chunk>) -> Module {
    Module {
        schema_hash: 0,
        enum_layouts: Vec::new(),
        signatures: Vec::new(),
        native_return_shapes: Vec::new(),
        chunks,
        native_names: Vec::new(),
        entry_point: Some(0),
        data_layout: None,
        word_bits_log2: RUNTIME_WORD_BITS_LOG2,
        addr_bits_log2: RUNTIME_ADDRESS_BITS_LOG2,
        float_bits_log2: RUNTIME_FLOAT_BITS_LOG2,
        wcet_cycles: 0,
        wcmu_bytes: 0,
        aux_arena_bytes: 0,
        persistent_composite_bytes: 0,
        flags: 0,
        shared_data_bytes: 0,
        private_data_bytes: 0,
    }
}

// Audit remediation (SECURITY_AUDIT_V0_2_1, poc_newarray_underflow,
// finding 3). A `NewComposite` array of ten elements on an empty operand
// stack would drain ten operands that are not present. The operand-stack-depth
// verifier pass now rejects it at load: `Vm::new` returns a `VerifyError`
// rather than constructing a VM whose execution would underflow. The VM's
// drain guard remains as defense in depth for `new_unchecked` loads.
#[test]
fn newarray_underflow_rejected_by_verifier() {
    let chunk = make_chunk(
        "main",
        vec![
            Op::NewComposite(keleusma::bytecode::NewCompositeOperand::Flat {
                kind: keleusma::value_layout::CompositeKind::Array,
                count: 10,
                byte_size: 80,
            }),
            Op::Return,
        ],
    );
    let module = make_module(vec![chunk]);
    let arena = Arena::with_capacity(DEFAULT_ARENA_CAPACITY);
    let res = Vm::new(module, &arena);
    assert!(
        matches!(res, Err(VmError::VerifyError(_))),
        "expected the verifier to reject the NewArray operand-stack underflow, got {:?}",
        res.map(|_| "Ok")
    );
}