On Tue, Sep 8, 2020 at 4:32 PM James Carter <jwcart2@xxxxxxxxx> wrote:
>
> On Tue, Sep 8, 2020 at 11:27 AM Stephen Smalley
> <stephen.smalley.work@xxxxxxxxx> wrote:
> >
> > On Tue, Sep 8, 2020 at 9:50 AM Stephen Smalley
> > <stephen.smalley.work@xxxxxxxxx> wrote:
> > >
> > > On Tue, Sep 8, 2020 at 9:46 AM Stephen Smalley
> > > <stephen.smalley.work@xxxxxxxxx> wrote:
> > > >
> > > > On Fri, Sep 4, 2020 at 8:49 AM Stephen Smalley
> > > > <stephen.smalley.work@xxxxxxxxx> wrote:
> > > > >
> > > > > On Thu, Sep 3, 2020 at 2:19 PM James Carter <jwcart2@xxxxxxxxx> wrote:
> > > > > >
> > > > > > CIL was not correctly determining the depth of constraint expressions
> > > > > > which prevented it from giving an error when the max depth was exceeded.
> > > > > > This allowed invalid policy binaries with constraint expressions exceeding
> > > > > > the max depth to be created.
> > > > > >
> > > > > > Correctly calculate the depth of constraint expressions when building
> > > > > > the AST and give an error when the max depth is exceeded.
> > > > > >
> > > > > > Reported-by: Jonathan Hettwer <j2468h@xxxxxxxxx>
> > > > > > Signed-off-by: James Carter <jwcart2@xxxxxxxxx>
> > > > >
> > > > > The fix for conditional boolean expression depth checking can be a
> > > > > separate patch. For this one,
> > > > >
> > > > > Acked-by: Stephen Smalley <stephen.smalley.work@xxxxxxxxx>
> > > >
> > > > Actually, this breaks selinux-testsuite. Will have to look into why.
> > > > /usr/sbin/semodule -i test_policy/test_policy.pp test_mlsconstrain.cil
> > > > test_overlay_defaultrange.cil test_add_levels.cil test_glblub.cil
> > > > Max depth of 4 exceeded for constraint expression
> > > > Bad expression tree for constraint
> > > > Bad constrain declaration at
> > > > /var/lib/selinux/targeted/tmp/modules/100/base/cil:919
> > >
> > > Here is the failing cil module:
> > > $ cat policy/test_mlsconstrain.cil
> > > (mlsconstrain (peer (recv)) (or (dom l1 l2) (and (neq t1
> > > mcs_constrained_type) (neq t2 mcs_constrained_type))))
> > > (mlsconstrain (packet (recv)) (or (dom l1 l2) (and (neq t1
> > > mcs_constrained_type) (neq t2 mcs_constrained_type))))
> > >
> > > Maybe an off-by-one in your depth checking?
> >
> > Actually, the depth computation logic doesn't seem consistent with
> > checkpolicy's define_constraint().
>
> I don't really understand what checkpolicy is doing. I guess keeping
> track of the postfix stack size?
Yes, the whole point is to prevent overflowing the fixed-size stack
used by the kernel (and by libsepol) in evaluating constraints.
Originally I think it was to bound recursion in the function since the
original implementation was recursive and only later converted. The
important thing is to match the kernel.
> The one difference that would be easy to fix is that checkpolicy ignores "not".
>
> CIL has a max depth = 4, but checkpolicy has a max depth = 0 for these:
> (constrain (C5 (P5)) (not (not (not (not (eq t1 T5a))))))
> constrain C5 { P5 } not (not (not (not (t1 == T5a))));
>
> Here is one pair of examples that would be hard for me to make CIL
> agree with checkpolicy. These are essentially the same constraint:
>
> Both see max depth = 2 for this one
> (constrain (C6 (P6)) (or (eq t1 T6g) (and (neq t1 A6a) (neq t2 T6f))))
> constrain C6 { P6 } (t1 == T6g or (t1 != A6a and t2 != T6f));
>
> CIL sees max depth = 2 for this one, but checkpolicy has max depth = 1
> (constrain (C7 (P7)) (or (and (neq t1 A7a) (neq t2 T7f)) (eq t1 T7g)))
> constrain C7 { P7 } ((t1 != A7a and t2 != T7f) or t1 == T7g);
>
> In most other examples that I have created, they had the same max depth.
>
> Both have max depth = 2 for these:
> (constrain (C1 (P1)) (or (eq t1 T1a) (and (eq t1 T1b) (eq t1 T1c))))
> constrain C1 { P1 } (t1 == T1a or (t1 == T1b and t1 == T1c));
>
> Both have max depth = 4 for these:
> (constrain (C2 (P2)) (or (eq t1 T2a) (or (eq t1 T2b) (or (eq t1 T2c)
> (and (eq t1 T2d) (eq t1 T2e))))))
> constrain C2 { P2 } (t1 == T2a or (t1 == T2b or (t1 == T2c or (t1 ==
> T2d and t1 == T2e))));
>
> Both have max depth = 3 for these:
> (constrain (C4 (P4)) (or (or (eq t1 T4a) (or (eq t1 T4b) (eq t1 T4c)))
> (or (eq t1 T4d) (and (eq t1 T4e) (eq t1 T4f)))))
> constrain C4 { P4 } ((t1 == T4a or (t1 == T4b or t1 == T4c)) or (t1 ==
> T4d or (t1 == T4e and t1 == T4f)));
>
> Both have max depth = 4 for these:
> (constrain (C8 (P8)) (or (or (or (and (neq t1 T8a) (neq t1 T8b)) (and
> (neq t1 T8c) (neq t1 T8d))) (or (and (neq t1 T8e) (neq t1 T8f)) (and
> (neq t1 T8g) (neq t1 T8h)))) (or (or (and (neq t1 T8i) (neq t1 T8j))
> (and (neq t1 T8k) (neq t1 T8l))) (or (and (neq t1 T8m) (neq t1 T8n))
> (and (neq t1 T8o) (neq t1 T8p))))))
> constrain C8 { P8 } ((((t1 != T8a and t1 != T8b) or (t1 != T8c and t1
> != T8d)) or ((t1 != T8e and t1 != T8f) or (t1 != T8g and t1 != T8h)))
> or (((t1 != T8i and t1 != T8j) or (t1 != T8k and t1 != T8l)) or ((t1
> != T8m and t1 != T8n) or (t1 != T8o and t1 != T8p))));
>
> I guess I can convert the expressions to postfix and then follow the
> logic of checkpolicy, but that seems to be a lot of work. Instead, I
> could add a second check when the binary is being created and the
> constraint expression has been turned into postfix already.
