search

ldn-softdev / jtc

JSON processing utility
MIT License
501 stars 33 forks source link

Past-the-end string parsing in extract_lexeme #17

Closed futile closed 4 years ago

futile commented 4 years ago

The first loop in extract_lexeme (link) will continue past the end of the given string if the last character before the terminating 0 is a backslash (e.g., ./jtc -w '[\\' Bookmarks).

This is because the presence of the backslash will cause the iterator to be increased twice, thus skipping the terminating null-byte.

This bug was found using Symbolic Execution techniques developed in the course of the SYMBIOSYS research project at COMSYS, RWTH Aachen University. This research is supported by the European Research Council (ERC) under the EU's Horizon 2020 Research and Innovation Programme grant agreement n. 647295 (SYMBIOSYS).

ldn-softdev commented 4 years ago

Hi Futile, thank you for catching this one, indeed, overlooked issue, luckily the fix is trivial.

btw, is SYMBIOSYS publicly available?

ldn-softdev commented 4 years ago

I have posted the quick fixes for both issues, thanks again for reporting those!

futile commented 4 years ago

Thanks for the quick confirmation! We are using a version of the KLEE symbolic execution engine (https://klee.github.io) with our implementation for C++ support, which is available from the existing PR: https://github.com/klee/klee/pull/966.

Thanks for the quick fixes! :)