How to avoid to return uninitialized value on VeriFast?

[Kiwamu Okabe]

Dear all,

I'm trying to avoid following issue by VeriFast:

* Security Advisory:
https://www.freebsd.org/security/advisories/FreeBSD-SA-20:03.thrmisc.asc
* Patch https://github.com/freebsd/freebsd/commit/685a165c4c0b975cb2819b7042e1ddbc6eb79c5d

```c
static void
__elfN(note_thrmisc)(void *arg, struct sbuf *sb, size_t *sizep)
{
struct thread *td;
elf_thrmisc_t thrmisc;

td = (struct thread *)arg;
if (sb != NULL) {
KASSERT(*sizep == sizeof(thrmisc), ("invalid size"));
bzero(&thrmisc._pad, sizeof(thrmisc._pad));
strcpy(thrmisc.pr_tname, td->td_name);
sbuf_bcat(sb, &thrmisc, sizeof(thrmisc));
```

This issue caused by:

1. Get `elf_thrmisc_t` value on stack
2. `bzero` initialize the member `_pad` of `elf_thrmisc_t` value only,
don't initialize the other members
3. `sbuf_bcat`send the `elf_thrmisc_t` value into user space
4. If user application do cure dump, the uninitialized member leaks
data in kernel space

VeriFast has some solution to avoid returning uninitialized value?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[bart....@cs.kuleuven.be]

VeriFast currently does not help you find this type of problems. It currently treats an uninitialized variable just like any other variable. This is not strictly compliant with the C standard, which states that if the program reads an uninitialized variable whose address is never taken, its behavior is undefined (C18 §6.3.2.1). (Interestingly, from this paragraph it seems that reading an uninitialized variable whose address is taken is not a problem.) So it would make sense for a future version of VeriFast to distinguish between initialized and uninitialized variables and not allow reading uninitialized variables.

[Kiwamu Okabe]

Thank you for your advice, which made it clear.
--
Kiwamu Okabe