Class: SeccompTools::Symbolic::Constraint

Inherits:
Object
  • Object
show all
Defined in:
lib/seccomp-tools/symbolic/constraint.rb

Overview

One fact that must hold for the executor to be on a particular path, e.g. A == 1 or data[16] & 0xffff != 0. Every conditional jump adds one Constraint to each branch it takes; the accumulated list is the "path condition" carried in State#path and reported on a Executor::Leaf.

A constraint keeps a lone constant on the right: BPF always compares the A register against X or k, but A itself may hold the constant (e.g. A = 5 compared against a data word +tax+'d into X earlier), and every consumer reads "expression op constant". So +Constraint.new(5, :>, word)+ normalizes to word < 5 at construction - the two spellings are one value.

Constant Summary collapse

MIRROR =

The same comparison with its two sides swapped: 5 > x is x < 5. The bit tests are symmetric (+&+ commutes).

{
  :== => :==, :!= => :!=, :> => :<, :>= => :<=, :< => :>, :<= => :>=, set: :set, unset: :unset
}.freeze

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(lhs, op, rhs) ⇒ Constraint

Returns a new instance of Constraint.

Parameters:



49
50
51
52
53
54
 
# File 'lib/seccomp-tools/symbolic/constraint.rb', line 49

def initialize(lhs, op, rhs)
  lhs, op, rhs = rhs, MIRROR[op], lhs if lhs.imm? && !rhs.imm? # keep the constant on the right
  @lhs = lhs
  @op = op
  @rhs = rhs
end

Instance Attribute Details

#lhs ⇒ Expr (readonly)

Returns The left-hand side (what is being tested).

Returns:

  • (Expr) —

    The left-hand side (what is being tested).



39
40
41
 
# File 'lib/seccomp-tools/symbolic/constraint.rb', line 39

def lhs
  @lhs
end

#op ⇒ Symbol (readonly)

Returns The comparison, one of :==, :!=, :>, :>=, :<, :<=, :set, :unset. +:set+/+:unset+ mean "some/none of these bits are set" (from a jset test).

Returns:

  • (Symbol) —

    The comparison, one of :==, :!=, :>, :>=, :<, :<=, :set, :unset. +:set+/+:unset+ mean "some/none of these bits are set" (from a jset test).



42
43
44
 
# File 'lib/seccomp-tools/symbolic/constraint.rb', line 42

def op
  @op
end

#rhs ⇒ Expr (readonly)

Returns The right-hand side (what it is compared against).

Returns:

  • (Expr) —

    The right-hand side (what it is compared against).



44
45
46
 
# File 'lib/seccomp-tools/symbolic/constraint.rb', line 44

def rhs
  @rhs
end

Class Method Details

.evaluate(value, op, k) ⇒ Boolean

Applies one of the constraint operators to concrete operands: the jset bit tests (+:set+/+:unset+) and the Integer comparisons. Stateless - used to evaluate a pinned constraint or a candidate value, without building a SeccompTools::Symbolic::Constraint.

Parameters:

  • value (Integer)
  • op (Symbol)
  • k (Integer)

Returns:

  • (Boolean) 


30
31
32
33
34
35
36
 
# File 'lib/seccomp-tools/symbolic/constraint.rb', line 30

def self.evaluate(value, op, k)
  case op
  when :set then !value.nobits?(k)
  when :unset then value.nobits?(k)
  else value.public_send(op, k) # the comparisons are all Integer methods
  end
end

Instance Method Details

#key ⇒ String

A string that uniquely identifies this constraint, for both equality and hashing; the expr op expr counterpart of Expr#key, injective for the same reason.

Returns:

  • (String) 


75
76
77
 
# File 'lib/seccomp-tools/symbolic/constraint.rb', line 75

def key
  @key ||= "#{lhs.key}#{op}#{rhs.key}"
end

#plain_data_eq?(offset = nil) ⇒ Boolean

Is this a word == constant fact - about the word at offset, when given?

Parameters:

  • offset (Integer?) (defaults to: nil)

Returns:

  • (Boolean) 


68
69
70
 
# File 'lib/seccomp-tools/symbolic/constraint.rb', line 68

def plain_data_eq?(offset = nil)
  op == :== && plain_data_fact?(offset)
end

#plain_data_fact?(offset = nil) ⇒ Boolean

Is this a fact about one plain data word compared against a constant - about the word at offset, when given? These are the facts rule-based consumers can reason about, e.g. the feasibility pruning in Symbolic::Executor.

Parameters:

  • offset (Integer?) (defaults to: nil)

Returns:

  • (Boolean) 


61
62
63
 
# File 'lib/seccomp-tools/symbolic/constraint.rb', line 61

def plain_data_fact?(offset = nil)
  lhs.plain_data? && rhs.imm? && (offset.nil? || lhs.offset == offset)
end