runtimeverification / runtimeverification/llvm-backend
Ill-sorted injection casues unpredicatable behavior
Nobody has claimed this yet.
- Dominant language
- C++
- Stars
- 43
- Forks
- 22
- PR merge metrics
- No merged PRs in 30d
Description
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.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by compiling test.k and running test-kompiled/interpreter with the input.kore reproducer, including the BYTES-SYNTAX variant. Compare injections using SortBool{}, SortInt{}, and SortBytes{} as the From-sort. Done means malformed injections terminate with a clear error message rather than segfaulting or producing corrupted values.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp
- Domain
- compilers, security
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 45/100