Re: [Caml-list] Any plans for supporting Intel CET in OCaml?

[Hendrik Boom <hendrik@topoi.pooq.com>]

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