external c functions incorrectly accepted as safe

I played a bit, and this compiles:

using <stdio.h>::{printf, scanf};

export fn main() -> int {
    char foo[2];

    scanf("%s", foo);
    printf("hello unsound %s\n", foo);
    return 0;
}

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.

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

this is fine
or require to be wrapped in an unsafe {} block
or be done like typescript where you can specify additional signatures for plain old C code.

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);

Navigation Menu

Repository navigation

external c functions incorrectly accepted as safe #22

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

external c functions incorrectly accepted as safe #22

Description

Activity

bitwave commented on Feb 11, 2020

aep commented on Feb 11, 2020

bitwave commented on Feb 12, 2020

peirick commented on Feb 12, 2020

fogti commented on Feb 13, 2020

aep commented on Mar 30, 2020

fogti commented on Mar 30, 2020

aep commented on May 27, 2020

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions