linux-kernel - Re: [PATCH RFC v2 net-next 10/16] bpf: add eBPF verifier

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <CAMEtUuygJoH+PBNksTwRHyRObCZixoTDFzmnHroErZHZLaGNbg@mail.gmail.com>
Date:	Thu, 24 Jul 2014 12:25:02 -0700
From:	Alexei Starovoitov <ast@...mgrid.com>
To:	Andy Lutomirski <luto@...capital.net>
Cc:	"David S. Miller" <davem@...emloft.net>,
	Ingo Molnar <mingo@...nel.org>,
	Linus Torvalds <torvalds@...ux-foundation.org>,
	Steven Rostedt <rostedt@...dmis.org>,
	Daniel Borkmann <dborkman@...hat.com>,
	Chema Gonzalez <chema@...gle.com>,
	Eric Dumazet <edumazet@...gle.com>,
	Peter Zijlstra <a.p.zijlstra@...llo.nl>,
	Arnaldo Carvalho de Melo <acme@...radead.org>,
	Jiri Olsa <jolsa@...hat.com>,
	Thomas Gleixner <tglx@...utronix.de>,
	"H. Peter Anvin" <hpa@...or.com>,
	Andrew Morton <akpm@...ux-foundation.org>,
	Kees Cook <keescook@...omium.org>,
	Linux API <linux-api@...r.kernel.org>,
	Network Development <netdev@...r.kernel.org>,
	"linux-kernel@...r.kernel.org" <linux-kernel@...r.kernel.org>
Subject: Re: [PATCH RFC v2 net-next 10/16] bpf: add eBPF verifier

On Thu, Jul 24, 2014 at 11:25 AM, Andy Lutomirski <luto@...capital.net> wrote:
> On Thu, Jul 17, 2014 at 9:20 PM, Alexei Starovoitov <ast@...mgrid.com> wrote:
>> Safety of eBPF programs is statically determined by the verifier, which detects:
>> - loops
>> - out of range jumps
>> - unreachable instructions
>> - invalid instructions
>> - uninitialized register access
>> - uninitialized stack access
>> - misaligned stack access
>> - out of range stack access
>> - invalid calling convention
>
> Is there something that documents exactly what conditions an eBPF
> program must satisfy in order to be considered valid?

I did a writeup in the past on things that verifiers checks and gave it
to internal folks to review. Guys have said that now they understand very
well how it works, but in reality it didn't help at all to write valid programs.
What worked is 'verification trace' = the instruction by instruction dump
of verifier state while it's analyzing the program.
I gave few simple examples of it in
'Understanding eBPF verifier messages' section:
https://git.kernel.org/cgit/linux/kernel/git/ast/bpf.git/diff/Documentation/networking/filter.txt?id=b22459133b9f52d2176c8c0f8b5eb036478a40c9
Every example there is what "program must satisfy to be valid"...

Therefore I'm addressing two things:
1. how verifier works and what it checks for.
  that is described in 'eBPF verifier' section of the doc and
  in 200 lines of comments inside verifier.c
2. how to write valid programs
 that's more important one, since it's a key to happy users.
 'verification trace' is the first step. I'm planning to add debug info and
 user space tool that points out to line in C instead of assembler trace.
 In other words to bring errors to user as early as possible during
 compilation process.
 This is not a concern when programs are written in assembler,
 since the programs will be much shorter and thought through by
 the author. However I don't think there will be too many users
 willing to understand ebpf assembler.

I suspect you're more concerned about #1 at this point whereas
I'm concerned about #2.
--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@...r.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/