kismet/kclause: false alarm in kismet due to incorrect representation of inequality constraints in kclause

[necipfazil]

Reproduce:

git checkout e9c5048c2de1913d0bcd589bc1487810c2e24bc1
kismet --selectees CONFIG_CRYPTO_DEV_FSL_CAAM_BLOB_GEN --selectors CONFIG_TRUSTED_KEYS_CAAM -a=arm64

The false alarm happens due to a constraint that involves inequality between options. See the following configuration option definition taken from security/keys/trusted-keys/Kconfig:

config TRUSTED_KEYS_CAAM
  bool "CAAM-based trusted keys"
  depends on CRYPTO_DEV_FSL_CAAM_JR >= TRUSTED_KEYS
  select CRYPTO_DEV_FSL_CAAM_BLOB_GEN
  default y
  help
    Enable use of NXP's Cryptographic Accelerator and Assurance Module
    (CAAM) as trusted key backend.

The dependency (CRYPTO_DEV_FSL_CAAM_JR >= TRUSTED_KEYS) suggests following assignment to be infeasible:

CONFIG_TRUSTED_KEYS_CAAM=y
# CONFIG_CRYPTO_DEV_FSL_CAAM_JR is not set
CONFIG_TRUSTED_KEYS=y

However, kclause's representation of the inequality in the dependency does have no effect, which make such assignment satisfiable. To reproduce this specific problem, use klocalizer, which says satisfiable:

klocalizer -a=arm64 -D CONFIG_TRUSTED_KEYS_CAAM -D CONFIG_TRUSTED_KEYS -U CONFIG_CRYPTO_DEV_FSL_CAAM_JR

[necipfazil]

kclause represents inequalities as a z3 compare predicate. However, the predicate has no effect over individual booleans. Below reproduces how kclause's representation misses this constraints.

Save the following as example.smt2:

; benchmark generated from python API                                      
(set-info :status unknown)                                                 
(declare-fun |PREDICATE_Compare(left=Name(id='CONFIG_CRYPTO_DEV_FSL_CAAM_JR', ctx=Load()), ops=[GtE()], comparators=[Name(id='CONFIG_TRUSTED_KEYS', ctx=Load())])| () Bool)
(declare-fun CONFIG_TRUSTED_KEYS () Bool)                                  
(declare-fun CONFIG_CRYPTO_DEV_FSL_CAAM_JR () Bool)                        
(assert                                                                    
 (let (($x111300 (and CONFIG_TRUSTED_KEYS |PREDICATE_Compare(left=Name(id='CONFIG_CRYPTO_DEV_FSL_CAAM_JR', ctx=Load()), ops=[GtE()], comparators=[Name(id='CONFIG_TRUSTED_KEYS', ctx=Load())])|)))
 (let (($x111301 (not CONFIG_CRYPTO_DEV_FSL_CAAM_JR)))                     
 (and $x111300 $x111301 ))))                                               
(check-sat)

Run the following python script, which will parse the above smt2 file, and do SAT check:

import z3                                                                  
                                                                           
# load model                                                               
clause = z3.parse_smt2_file("example.smt2")                                
print("clause is:\n==\n%s\n==\n" % clause)                                 
                                                                           
# sat check                                                                
s = z3.Solver()                                                            
s.add(clause)                                                              
check_sat = s.check()                                                      
                                                                           
print("Sat check result: %s" % check_sat)                                  
                                                                           
# get model                                                                
m = s.model()                                                              
print("model:\n==\n%s\n==\n" % m)

It will print:

clause is:
==
[And(And(CONFIG_TRUSTED_KEYS,
         PREDICATE_Compare(left=Name(id='CONFIG_CRYPTO_DEV_FSL_CAAM_JR', ctx=Load()), ops=[GtE()], comparators=[Name(id='CONFIG_TRUSTED_KEYS', ctx=Load())])),
     Not(CONFIG_CRYPTO_DEV_FSL_CAAM_JR))]
==

Sat check result: sat
model:
==
[PREDICATE_Compare(left=Name(id='CONFIG_CRYPTO_DEV_FSL_CAAM_JR', ctx=Load()), ops=[GtE()], comparators=[Name(id='CONFIG_TRUSTED_KEYS', ctx=Load())]) = True,
 CONFIG_TRUSTED_KEYS = True,
 CONFIG_CRYPTO_DEV_FSL_CAAM_JR = False]
==

As can be seen, with kclause's representation of the inequality (CONFIG_CRYPTO_DEV_FSL_CAAM_JR >= CONFIG_TRUSTED_KEYS), the assignment CONFIG_TRUSTED_KEYS = True, CONFIG_CRYPTO_DEV_FSL_CAAM_JR = False shown to be satisfiable, which is in fact unsatisfiable.

[necipfazil]

Partial fix suggestion: As we represent tristates as booleans, we may not capture inequalities in full precision. However, we could still improve the inequality constraints. For example, for > and >=, we can instead use implication: A >= B would translate to B implies A.