Open bitwave opened 4 years ago
Another example:
using <stdio.h>::{printf, scanf};
export fn main() -> int {
char *foo = 0x1337;
printf("hello unsound %s\n", foo);
return 0;
}
This is even simpler and simply unsafe.
thank you for the report. calls to libc functions cannot be proven, because they have no zz signatures. therefor the checker is just disabled on any expression containing an external C type
still unsure if
If you focusing on safety, everything which is not proven or assumed explicitely, should be unsafe.
i would go with an explicit unsafe block.
It should at least emit a warning, especially for known-unsafe c functions (e.g. like scanf
on strings, gets
, etc.).
References:
inherently vulnerable/unsafe C functions:
gets
getpw
rewind
, setbuf
strcat
, strcpy
sprintf
this is currently blocked because an unsafe block is a scope, so this is not possible:
unsafe {
int i = some_c_function();
}
int x = i;
and initialization in unsafe breaks SMT.
int i;
unsafe {
i = some_c_function();
}
int x = i; // uninitialized read access
i'll either need to make unsafe an expression instead of a scope
int i = unsafe {
some_c_function()
};
int x = i;
which means you need to wrap every call in unsafe rather than an entire list of statements.
or make it a block but ignore scoping so this is valid but harder to understand:
unsafe {
int i = some_c_function();
}
int x = i;
another option is forcing c calls through a macro
int i = @extern(some_c_function());
int x = i;
the macro can do additional checks in first class library code rather than in the compiler
Could it be possible to make unsafe
an expression, and for the less often needed block-unsafe add an unsafe_block
, which creates an own scope?
unsafe is now available in expression position:
int e = unsafe<int>(errno);
I played a bit, and this compiles:
this should be unsound for len(stdin) > 2 or 1 (depends on NUL-byte or not) ASAN finds this at runtime, but it feels unsound.