How to avoid to return uninitialized value on ATS2?

[Kiwamu Okabe]

Dear all,

I try to avoid following issue using ATS2:

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

This issue is caused by returning uninitialized value into user space
from FreeBSD kernel.
Then I wrote following pseudo code:

https://github.com/metasepi/postmortem/blob/master/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:03.thrmisc/Resolution/ATS2/error/main.dats

Above code can't avoid this issue with at-view.

* `!a? @ l >> a @ l` means to initialize uninitialized value
* `!a @ l` means to take and keep initialized or uninitialized value

How to explain to take "uninitialized value" as type?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Kiwamu Okabe]

On Wed, Sep 16, 2020 at 4:10 PM Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> * `!a? @ l >> a @ l` means to initialize uninitialized value
> * `!a @ l` means to take and keep initialized or uninitialized value
>
> How to explain to take "uninitialized value" as type?

Sorry. I would like to know how to take ***initialized*** value only.

[Hongwei Xi]

It works because the type for sbuf_bcat allows it:

val () = sbuf_bcat{elf_thrmisc_t}(pf_thrmisc | addr_thrmisc) // fails

val () = sbuf_bcat{elf_thrmisc_t?}(pf_thrmisc | addr_thrmisc) // succeeds

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3Dkyay10uEqkyzgJoWOYe-ToHGtLv08m2QREbp%2BbWLt-w%40mail.gmail.com.

[Kiwamu Okabe]

Dear Hongwei,

On Wed, Sep 16, 2020 at 8:30 PM Hongwei Xi <gmh...@gmail.com> wrote:
> It works because the type for sbuf_bcat allows it:
>
> val () = sbuf_bcat{elf_thrmisc_t}(pf_thrmisc | addr_thrmisc) // fails
> val () = sbuf_bcat{elf_thrmisc_t?}(pf_thrmisc | addr_thrmisc) // succeeds

On my project, following code should be failed:

```ats
fun note_thrmisc(): void = {
var thrmisc: elf_thrmisc_t

// Don't call `bzero` function

prval pf_thrmisc = view@thrmisc
val addr_thrmisc = addr@thrmisc
val () = sbuf_bcat(pf_thrmisc | addr_thrmisc) // <= Should fail
prval () = view@thrmisc:= pf_thrmisc
}
```

because the `sbuf_bcat` function returns uninitialized value `thrmisc`
into user space.
If `thrmisc` was initialized by `bzero` function, the `sbuf_bcat`
function should succeed.


On my project, firstly I write code which should fail to find C
language errors such as following:
https://github.com/metasepi/postmortem/blob/master/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-19:15.mqueuefs/Resolution/ATS2/error/main.dats

And secondly I fix the errors as following:
https://github.com/metasepi/postmortem/blob/master/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-19:15.mqueuefs/Resolution/ATS2/fix/main.dats

This mail issue is about the former.

[Hongwei Xi]

>>fun sbuf_bcat {a:vt@ype}{l:addr} (pf: !a @ l | p: ptr l): void

The type of sbuf_bcat does NOT say anything about 'a'. So 'a' can

actually be instantiated with an uninitialized type.

If you change the type of sbuf_bcat as follows:

fun sbuf_bcat {l:addr} (elf_thrmisc_t @ l | ptr (l)): void

then a type-error will be reported.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnQ-MXMNy3h89oxB9T8Q2dZVEwXO-VhEO-kVHaKrVTHpA%40mail.gmail.com.

[Kiwamu Okabe]

Dear Hongwei,

On Thu, Sep 17, 2020 at 10:46 AM Hongwei Xi <gmh...@gmail.com> wrote:
> >>fun sbuf_bcat {a:vt@ype}{l:addr} (pf: !a @ l | p: ptr l): void
>
> The type of sbuf_bcat does NOT say anything about 'a'. So 'a' can
> actually be instantiated with an uninitialized type.

Thanks. Your advice fixed my miss-understanding.

> If you change the type of sbuf_bcat as follows:
>
> fun sbuf_bcat {l:addr} (elf_thrmisc_t @ l | ptr (l)): void
>
> then a type-error will be reported.

Thanks. Your patch proved FreeBSD-SA-20:03.thrmisc:

https://github.com/metasepi/postmortem/commit/295cc4b899e7c79b524b9ba5512999687cd5c868

BTW. Can we create a polymorphic `sbuf_bcat` function to avoid
returning uninitialized value?
The `sbuf_bcat` function is defined with C language in FreeBSD such as
following:

```c
int
sbuf_bcat(struct sbuf *s, const void *buf, size_t len)
```

It means `sbuf_bcat` can take any type with `buf` more than `elf_thrmisc_t`.

[Hongwei Xi]

>>BTW. Can we create a polymorphic `sbuf_bcat` function to avoid
>>returning uninitialized value?

You can do something like:

   absprop INITIALIZED(a:vt@ype)

   fun

   sbuf_bcat
   {a:vt@ype}{l:addr}

   (pf0: INITIALIZED(a), pf1: !a @ l | p: ptr l): void = undefined()

The problem with this approach is that the user of sbuf_bcat is burdened with

the need for explicitly constructing a proof to show that 'a' is initialized.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnzkR6JCUivUFr4Xem-Qhzg%3DqrhyP1isEGXD18L8Wixbw%40mail.gmail.com.

[Kiwamu Okabe]

Dear Hongwei,

On Thu, Sep 17, 2020 at 9:51 PM Hongwei Xi <gmh...@gmail.com> wrote:
> >>BTW. Can we create a polymorphic `sbuf_bcat` function to avoid
> >>returning uninitialized value?
>
> You can do something like:
>
> absprop INITIALIZED(a:vt@ype)
>
> fun
> sbuf_bcat
> {a:vt@ype}{l:addr}
> (pf0: INITIALIZED(a), pf1: !a @ l | p: ptr l): void = undefined()

Oh, `absprop`. But...

> The problem with this approach is that the user of sbuf_bcat is burdened with
> the need for explicitly constructing a proof to show that 'a' is initialized.

I can't understand this clearly.
Should I introduce `INITIALIZED(a)` with some proof function as the user?

[Artyom Shalkhakov]

пт, 18 сент. 2020 г. в 02:00, Kiwamu Okabe <kiw...@debian.or.jp>:

Hongwei, what does the `?` syntax stand for? Is it a type constructor? Is it something of the sort vt0ype -> t0ype, so that, together with the axiom(?) that any type is a viewtype with an empty view part, gives us this behavior? Are there any special rules to it?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmvx%3Dj%2B1cGF7%2BOSbUNXUiOuNkTvzb20MbvFDtozRynJRA%40mail.gmail.com.

--

Cheers,
Artyom Shalkhakov

[gmhwxi]

>>what does the `?` syntax stand for?

Given a viewt@ype VT, VT? (? is a postfix operator here)  is a t@ype such that

sizeof(VT) = sizeof(VT?).

? : viewt@ype -> t@ype // this is the sort assigned to '?'

Note that VT? is completely opaque; the only information on VT? is its size.