caml-list - the Caml user's mailing list
 help / Atom feed
* [Caml-list] Any plans for supporting Intel CET in OCaml?
@ 2019-07-25 14:28 Richard W.M. Jones
  2019-07-25 15:52 ` Gerd Stolpmann
  2019-07-31 12:05 ` Xavier Leroy
  0 siblings, 2 replies; 7+ messages in thread
From: Richard W.M. Jones @ 2019-07-25 14:28 UTC (permalink / raw)
  To: caml-list; +Cc: nickc

There's an effort to harden every binary in RHEL to protect against
ROP-style attacks.  Of course this is mainly applicable when your
language is vulnerable to buffer overflows, but sadly even our OCaml
applications still link to some C libraries :-(

I was looking into this and the indirect branch tracking (IBT) part
seems simple enough.  For every indirect jump or call _target_ you
must insert one of the two instructions ENDBR64 or ENDBR32 (both are
NOP-like on older processors).  The processor sets a flag when an
indirect jump is taken and #CP's if the indirect jump doesn't land on
one of these instructions.

There's also some stuff with shadow stacks which looks a lot more
complicated and I didn't fully understand.  The whole thing is
described in:

https://software.intel.com/sites/default/files/managed/4d/2a/control-flow-enforcement-technology-preview.pdf
https://lwn.net/Articles/758245/

Unfortunately (but for obvious reasons) every asm object in a program
must be compiled with CET in order to enable the feature for the
program as a whole.  This means that any mixed OCaml/C program can't
benefit from CET even in the C parts, unless we also support this in
the OCaml parts.

Has anyone looked into supporting this kind of thing in the amd64
backend?

(I looked at the OCaml trunk and couldn't see any relevant commits,
but maybe I missed something in my grepping).

Rich.

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [Caml-list] Any plans for supporting Intel CET in OCaml?
  2019-07-25 14:28 [Caml-list] Any plans for supporting Intel CET in OCaml? Richard W.M. Jones
@ 2019-07-25 15:52 ` Gerd Stolpmann
  2019-07-25 19:24   ` Hendrik Boom
  2019-07-31 12:05 ` Xavier Leroy
  1 sibling, 1 reply; 7+ messages in thread
From: Gerd Stolpmann @ 2019-07-25 15:52 UTC (permalink / raw)
  To: caml-list

[-- Attachment #1.1: Type: text/plain, Size: 2990 bytes --]

Am 25.07.19 um 16:28 schrieb Richard W.M. Jones:
> There's an effort to harden every binary in RHEL to protect against
> ROP-style attacks.  Of course this is mainly applicable when your
> language is vulnerable to buffer overflows, but sadly even our OCaml
> applications still link to some C libraries :-(
>
> I was looking into this and the indirect branch tracking (IBT) part
> seems simple enough.  For every indirect jump or call _target_ you
> must insert one of the two instructions ENDBR64 or ENDBR32 (both are
> NOP-like on older processors).  The processor sets a flag when an
> indirect jump is taken and #CP's if the indirect jump doesn't land on
> one of these instructions.

I guess that's fairly simple to add: Just put these instructions at the
beginning of each function, and you're good. For local functions, you
could do a bit more analysis to find those that are really used as branch
targets. If I understand it correctly, the idea of CET is to reduce the
attack surface.

>
> There's also some stuff with shadow stacks which looks a lot more
> complicated and I didn't fully understand.  The whole thing is
> described in:

I think the idea is to prevent that you can change the return addresses
on the stack. For most code this should be fairly automatic, with a
few exceptions. The first is long jumps (used for exceptions in OCaml).
I've seen that there's a special instruction for removing entries from
the shadow stack, and for doing a long jump you need to know how many
frames you are going back.

The other area where this could fall on your feet are structural
transitions where you write new stack entries, e.g. when you need to
switch to different calling conventions and need to write completely new
frames including return addresses. You cannot write new return addresses
to the shadow stack, though. I don't know by heart whether this affects
OCaml, but it could.

Gerd


>
> https://software.intel.com/sites/default/files/managed/4d/2a/control-flow-enforcement-technology-preview.pdf
> https://lwn.net/Articles/758245/
>
> Unfortunately (but for obvious reasons) every asm object in a program
> must be compiled with CET in order to enable the feature for the
> program as a whole.  This means that any mixed OCaml/C program can't
> benefit from CET even in the C parts, unless we also support this in
> the OCaml parts.
>
> Has anyone looked into supporting this kind of thing in the amd64
> backend?
>
> (I looked at the OCaml trunk and couldn't see any relevant commits,
> but maybe I missed something in my grepping).
>
> Rich.

-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------



[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 488 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [Caml-list] Any plans for supporting Intel CET in OCaml?
  2019-07-25 15:52 ` Gerd Stolpmann
@ 2019-07-25 19:24   ` Hendrik Boom
  0 siblings, 0 replies; 7+ messages in thread
From: Hendrik Boom @ 2019-07-25 19:24 UTC (permalink / raw)
  To: caml-list

On Thu, Jul 25, 2019 at 05:52:06PM +0200, Gerd Stolpmann wrote:
> Am 25.07.19 um 16:28 schrieb Richard W.M. Jones:
> > There's an effort to harden every binary in RHEL to protect against
> > ROP-style attacks.  Of course this is mainly applicable when your
> > language is vulnerable to buffer overflows, but sadly even our OCaml
> > applications still link to some C libraries :-(
> >
> > I was looking into this and the indirect branch tracking (IBT) part
> > seems simple enough.  For every indirect jump or call _target_ you
> > must insert one of the two instructions ENDBR64 or ENDBR32 (both are
> > NOP-like on older processors).  The processor sets a flag when an
> > indirect jump is taken and #CP's if the indirect jump doesn't land on
> > one of these instructions.
> 
> I guess that's fairly simple to add: Just put these instructions at the
> beginning of each function, and you're good. For local functions, you
> could do a bit more analysis to find those that are really used as branch
> targets. If I understand it correctly, the idea of CET is to reduce the
> attack surface.
> 
> >
> > There's also some stuff with shadow stacks which looks a lot more
> > complicated and I didn't fully understand.  The whole thing is
> > described in:
> 
> I think the idea is to prevent that you can change the return addresses
> on the stack. For most code this should be fairly automatic, with a
> few exceptions. The first is long jumps (used for exceptions in OCaml).
> I've seen that there's a special instruction for removing entries from
> the shadow stack, and for doing a long jump you need to know how many
> frames you are going back.
> 
> The other area where this could fall on your feet are structural
> transitions where you write new stack entries, e.g. when you need to
> switch to different calling conventions and need to write completely new
> frames including return addresses. You cannot write new return addresses
> to the shadow stack, though. I don't know by heart whether this affects
> OCaml, but it could.

I wonder how the shadow stack interacts with tail recursion.

-- hendrik

> 
> Gerd
> 
> 
> >
> > https://software.intel.com/sites/default/files/managed/4d/2a/control-flow-enforcement-technology-preview.pdf
> > https://lwn.net/Articles/758245/
> >
> > Unfortunately (but for obvious reasons) every asm object in a program
> > must be compiled with CET in order to enable the feature for the
> > program as a whole.  This means that any mixed OCaml/C program can't
> > benefit from CET even in the C parts, unless we also support this in
> > the OCaml parts.
> >
> > Has anyone looked into supporting this kind of thing in the amd64
> > backend?
> >
> > (I looked at the OCaml trunk and couldn't see any relevant commits,
> > but maybe I missed something in my grepping).
> >
> > Rich.
> 
> -- 
> ------------------------------------------------------------
> Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
> My OCaml site:          http://www.camlcity.org
> Contact details:        http://www.camlcity.org/contact.html
> Company homepage:       http://www.gerd-stolpmann.de
> ------------------------------------------------------------
> 
> 




^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [Caml-list] Any plans for supporting Intel CET in OCaml?
  2019-07-25 14:28 [Caml-list] Any plans for supporting Intel CET in OCaml? Richard W.M. Jones
  2019-07-25 15:52 ` Gerd Stolpmann
@ 2019-07-31 12:05 ` Xavier Leroy
  2019-07-31 14:19   ` Hendrik Boom
  1 sibling, 1 reply; 7+ messages in thread
From: Xavier Leroy @ 2019-07-31 12:05 UTC (permalink / raw)
  To: Richard W.M. Jones; +Cc: caml users, nickc

[-- Attachment #1: Type: text/plain, Size: 1771 bytes --]

On Thu, Jul 25, 2019 at 4:28 PM Richard W.M. Jones <rich@annexia.org> wrote:

> There's an effort to harden every binary in RHEL to protect against
> ROP-style attacks.  Of course this is mainly applicable when your
> language is vulnerable to buffer overflows, but sadly even our OCaml
> applications still link to some C libraries :-(
>
> I was looking into this and the indirect branch tracking (IBT) part
> seems simple enough.  For every indirect jump or call _target_ you
> must insert one of the two instructions ENDBR64 or ENDBR32 (both are
> NOP-like on older processors).  The processor sets a flag when an
> indirect jump is taken and #CP's if the indirect jump doesn't land on
> one of these instructions.
>

Sounds like it should be easy to add to the OCaml x86-64 back-end.


>
> There's also some stuff with shadow stacks which looks a lot more
> complicated and I didn't fully understand.  The whole thing is
> described in:
>
>
> https://software.intel.com/sites/default/files/managed/4d/2a/control-flow-enforcement-technology-preview.pdf
> https://lwn.net/Articles/758245/
>
>
I don't understand how these shadow stacks are supposed to interact with
exception handling, either Caml-style or C++/Java style.

Kind regards,

- Xavier Leroy


> Unfortunately (but for obvious reasons) every asm object in a program
> must be compiled with CET in order to enable the feature for the
> program as a whole.  This means that any mixed OCaml/C program can't
> benefit from CET even in the C parts, unless we also support this in
> the OCaml parts.
>
> Has anyone looked into supporting this kind of thing in the amd64
> backend?
>
> (I looked at the OCaml trunk and couldn't see any relevant commits,
> but maybe I missed something in my grepping).
>
> Rich.
>

[-- Attachment #2: Type: text/html, Size: 2815 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [Caml-list] Any plans for supporting Intel CET in OCaml?
  2019-07-31 12:05 ` Xavier Leroy
@ 2019-07-31 14:19   ` Hendrik Boom
  2019-07-31 15:21     ` Xavier Leroy
  0 siblings, 1 reply; 7+ messages in thread
From: Hendrik Boom @ 2019-07-31 14:19 UTC (permalink / raw)
  To: caml-list

On Wed, Jul 31, 2019 at 02:05:26PM +0200, Xavier Leroy wrote:
> On Thu, Jul 25, 2019 at 4:28 PM Richard W.M. Jones <rich@annexia.org> wrote:
> 
> > There's an effort to harden every binary in RHEL to protect against
> > ROP-style attacks.  Of course this is mainly applicable when your
> > language is vulnerable to buffer overflows, but sadly even our OCaml
> > applications still link to some C libraries :-(
> >
> > I was looking into this and the indirect branch tracking (IBT) part
> > seems simple enough.  For every indirect jump or call _target_ you
> > must insert one of the two instructions ENDBR64 or ENDBR32 (both are
> > NOP-like on older processors).  The processor sets a flag when an
> > indirect jump is taken and #CP's if the indirect jump doesn't land on
> > one of these instructions.
> >
> 
> Sounds like it should be easy to add to the OCaml x86-64 back-end.

There is, of course, also the question what would happen on nonintel or 
older  machines if they don't have those ENDBR64 or ENDBR32 
instructions in the hardware.

(Such as, perhaps, an actual AMD-manufactured AMD64?  Like my 
10-year-old AMD server?)

Do we now have two distinct platforms to support?

-- hendrik

> 
> 
> >
> > There's also some stuff with shadow stacks which looks a lot more
> > complicated and I didn't fully understand.  The whole thing is
> > described in:
> >
> >
> > https://software.intel.com/sites/default/files/managed/4d/2a/control-flow-enforcement-technology-preview.pdf
> > https://lwn.net/Articles/758245/
> >
> >
> I don't understand how these shadow stacks are supposed to interact with
> exception handling, either Caml-style or C++/Java style.
> 
> Kind regards,
> 
> - Xavier Leroy
> 
> 
> > Unfortunately (but for obvious reasons) every asm object in a program
> > must be compiled with CET in order to enable the feature for the
> > program as a whole.  This means that any mixed OCaml/C program can't
> > benefit from CET even in the C parts, unless we also support this in
> > the OCaml parts.
> >
> > Has anyone looked into supporting this kind of thing in the amd64
> > backend?
> >
> > (I looked at the OCaml trunk and couldn't see any relevant commits,
> > but maybe I missed something in my grepping).
> >
> > Rich.
> >

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [Caml-list] Any plans for supporting Intel CET in OCaml?
  2019-07-31 14:19   ` Hendrik Boom
@ 2019-07-31 15:21     ` Xavier Leroy
  2019-07-31 17:40       ` Ivan Gotovchits
  0 siblings, 1 reply; 7+ messages in thread
From: Xavier Leroy @ 2019-07-31 15:21 UTC (permalink / raw)
  To: Hendrik Boom; +Cc: caml users

[-- Attachment #1: Type: text/plain, Size: 1839 bytes --]

On Wed, Jul 31, 2019 at 4:20 PM Hendrik Boom <hendrik@topoi.pooq.com> wrote:

>
> There is, of course, also the question what would happen on nonintel or
> older  machines if they don't have those ENDBR64 or ENDBR32
> instructions in the hardware.
>

I read somewhere that those instructions look like no-ops on older
machines.

>
> (Such as, perhaps, an actual AMD-manufactured AMD64?  Like my
> 10-year-old AMD server?)
>
> Do we now have two distinct platforms to support?
>

It could be a configure-time choice.  I wouldn't call that two distinct
platforms, more like two variants of the same platform.

Just speculating here.  All this needs to be discussed and agreed on, of
course.

- Xavier Leroy


> -- hendrik
>
> >
> >
> > >
> > > There's also some stuff with shadow stacks which looks a lot more
> > > complicated and I didn't fully understand.  The whole thing is
> > > described in:
> > >
> > >
> > >
> https://software.intel.com/sites/default/files/managed/4d/2a/control-flow-enforcement-technology-preview.pdf
> > > https://lwn.net/Articles/758245/
> > >
> > >
> > I don't understand how these shadow stacks are supposed to interact with
> > exception handling, either Caml-style or C++/Java style.
> >
> > Kind regards,
> >
> > - Xavier Leroy
> >
> >
> > > Unfortunately (but for obvious reasons) every asm object in a program
> > > must be compiled with CET in order to enable the feature for the
> > > program as a whole.  This means that any mixed OCaml/C program can't
> > > benefit from CET even in the C parts, unless we also support this in
> > > the OCaml parts.
> > >
> > > Has anyone looked into supporting this kind of thing in the amd64
> > > backend?
> > >
> > > (I looked at the OCaml trunk and couldn't see any relevant commits,
> > > but maybe I missed something in my grepping).
> > >
> > > Rich.
> > >
>

[-- Attachment #2: Type: text/html, Size: 3101 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [Caml-list] Any plans for supporting Intel CET in OCaml?
  2019-07-31 15:21     ` Xavier Leroy
@ 2019-07-31 17:40       ` Ivan Gotovchits
  0 siblings, 0 replies; 7+ messages in thread
From: Ivan Gotovchits @ 2019-07-31 17:40 UTC (permalink / raw)
  To: Xavier Leroy; +Cc: Hendrik Boom, caml users

[-- Attachment #1: Type: text/plain, Size: 2977 bytes --]

On Wed, Jul 31, 2019 at 11:21 AM Xavier Leroy <
xavier.leroy@college-de-france.fr> wrote:

> On Wed, Jul 31, 2019 at 4:20 PM Hendrik Boom <hendrik@topoi.pooq.com>
> wrote:
>
>>
>> There is, of course, also the question what would happen on nonintel or
>> older  machines if they don't have those ENDBR64 or ENDBR32
>> instructions in the hardware.
>>
>
> I read somewhere that those instructions look like no-ops on older
> machines.
>

The `endbr64` is encoded as `f3 0f 1e fa` which [1] is a hintable [2]
opcode prefixed with `repz`, e.g., something like ` repz nop %edx`. Though
theoretically `0f 1e fa` should be considered as a nop
by most more or less modern CPU it is not really guaranteed, so whether it
will work on old AMD/Cyrix/etc is a big question (I bet no). Not to say
that the `f3` prefix complicates things even more.
The truth is that the introduction of `endrbr` actually broke most of the
code analyzers and emulators, e.g., LLVM, QEMU, Valgrind to name a few.


[1]: http://ref.x86asm.net/geek.html#x0F1E
[2]:
http://patft.uspto.gov/netacgi/nph-Parser?Sect2=PTO1&Sect2=HITOFF&p=1&u=/netahtml/PTO/search-bool.html&r=1&f=G&l=50&d=PALL&RefSrch=yes&Query=PN/5701442


>
>> (Such as, perhaps, an actual AMD-manufactured AMD64?  Like my
>> 10-year-old AMD server?)
>>
>> Do we now have two distinct platforms to support?
>>
>
> It could be a configure-time choice.  I wouldn't call that two distinct
> platforms, more like two variants of the same platform.
>
> Just speculating here.  All this needs to be discussed and agreed on, of
> course.
>
> - Xavier Leroy
>
>
>> -- hendrik
>>
>> >
>> >
>> > >
>> > > There's also some stuff with shadow stacks which looks a lot more
>> > > complicated and I didn't fully understand.  The whole thing is
>> > > described in:
>> > >
>> > >
>> > >
>> https://software.intel.com/sites/default/files/managed/4d/2a/control-flow-enforcement-technology-preview.pdf
>> > > https://lwn.net/Articles/758245/
>> > >
>> > >
>> > I don't understand how these shadow stacks are supposed to interact with
>> > exception handling, either Caml-style or C++/Java style.
>> >
>>
>
They are not supposed to. C++ exceptions, setjmp/longjmp, signal handlers,
etc are not covered by this technology. So the compiler should be clever
enough no to enable shadow stack if any of these features are used.


> > Kind regards,
>> >
>> > - Xavier Leroy
>> >
>> >
>> > > Unfortunately (but for obvious reasons) every asm object in a program
>> > > must be compiled with CET in order to enable the feature for the
>> > > program as a whole.  This means that any mixed OCaml/C program can't
>> > > benefit from CET even in the C parts, unless we also support this in
>> > > the OCaml parts.
>> > >
>> > > Has anyone looked into supporting this kind of thing in the amd64
>> > > backend?
>> > >
>> > > (I looked at the OCaml trunk and couldn't see any relevant commits,
>> > > but maybe I missed something in my grepping).
>> > >
>> > > Rich.
>> > >
>>
>

[-- Attachment #2: Type: text/html, Size: 5463 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

end of thread, back to index

Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-07-25 14:28 [Caml-list] Any plans for supporting Intel CET in OCaml? Richard W.M. Jones
2019-07-25 15:52 ` Gerd Stolpmann
2019-07-25 19:24   ` Hendrik Boom
2019-07-31 12:05 ` Xavier Leroy
2019-07-31 14:19   ` Hendrik Boom
2019-07-31 15:21     ` Xavier Leroy
2019-07-31 17:40       ` Ivan Gotovchits

caml-list - the Caml user's mailing list

Archives are clonable:
	git clone --mirror http://inbox.vuxu.org/caml-list
	git clone --mirror https://inbox.ocaml.org/caml-list

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.caml-list


AGPL code for this site: git clone https://public-inbox.org/ public-inbox