Skip to content

Ill-sorted injection casues unpredicatable behavior #1171

@tothtamas28

Description

@tothtamas28

Consider

// test.k
module TEST
endmoule

and

// input.kore
Lbl'-LT-'generatedTop'-GT-'{}(
    Lbl'-LT-'k'-GT-'{}(
        kseq{}(
            inj{SortBool{}, SortKItem{}}(\dv{SortBool{}}("false")),
            dotk{}()
        )
    ),
    Lbl'-LT-'generatedCounter'-GT-'{}(
        \dv{SortInt{}}("0")
    )
)

When running this program:

$ test-kompiled/interpreter input.kore 0 /dev/stdout

the result is as expected:

Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBool{}, SortKItem{}}(\dv{SortBool{}}("false")),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))

However, changing the From-sort of the injection to SortInt{} sometimes causes a segfault:

[1]    15017 segmentation fault (core dumped)  test-kompiled/interpreter input.kore 0 /dev/stdout

and sometimes results in successful termination with a well-sorted configuration containing a huge integer:

Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("<huge integer>")),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))

When the From-sort is SortBytes{} (requires importing BYTES-SYNTAX in TEST):

Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBytes{}, SortKItem{}}(\dv{SortBytes{}}("\xe0\x00 *\x14\x7f\x00<repeating \x00>\x00[1]    15733 segmentation fault (core dumped)  test-kompiled/interpreter input.kore 0 /dev/stdout

This behavior is not robust and is potentially insecure. Ideally, the interpreter should exit with an error message.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions