eyeprolog

Context schema audit

Which fields in a message do not fit the schema?

Two sensor messages each carry a bundle of fields with different shapes. One generic rule takes every field apart, measures its name and number of arguments, and compares that shape with an allowed schema. It never needs to know the field names in advance.

Run it in the playground · Source

The question

Incoming data is often heterogeneous: a heartbeat with no arguments, a source with one, a temperature with two, a GPS fix with three. A validator should catch a field with the wrong shape, such as a GPS fix missing its longitude, or a field that should not be there at all.

Can one rule audit every field, whatever its name or size?

Two messages and a schema

message_context(msg_bad, (
  heartbeat,
  source(sensor18),
  temperature(sensor18, 99),
  gps(sensor18, 51),
  tampered(sensor18)
)).

allowed_shape(heartbeat, 0).
allowed_shape(source, 1).
allowed_shape(temperature, 2).
allowed_shape(gps, 3).
allowed_shape(signature, 4).

msg_bad has two problems: gps has two arguments instead of three, and tampered is not in the schema. (msg_ok carries five well-formed fields.)

One generic rule

context_shape(Message, Name, Arity) :-
  message_context(Message, Context),
  context_member(Context, Statement),
  (Statement =.. [Name | Args]),
  length(Args, Arity).

schema_violation(Message, Name, Arity) :-
  context_shape(Message, Name, Arity),
  \+ allowed_shape(Name, Arity).

=.. turns gps(sensor18, 51) into the list [gps, sensor18, 51]. The head of the list is the name, and the length of the rest is the arity. A violation is a shape the schema does not allow.

The answer

eyeprolog examples/context-schema-audit.pl

context_shape(msg_bad, gps, 2).
context_shape(msg_bad, tampered, 1).
schema_violation(msg_bad, gps, 2).
schema_violation(msg_bad, tampered, 1).

That is an excerpt of 12 answers: ten context_shape/3 facts (five per message) and two violations, both in msg_bad. msg_ok passes cleanly.

The reason

eyeprolog --proof examples/context-schema-audit.pl

step(schema_violation(msg_bad, gps, 2),
     rule(12),
     ['Message' = msg_bad, 'Name' = gps, 'Arity' = 2],
     [context_shape(msg_bad, gps, 2), \+ allowed_shape(gps, 2)]).
step(\+ allowed_shape(gps, 2), absent, [], []).

The violation rests on two things: the measured shape gps/2, and the absence of an allowed_shape(gps, 2) fact. That second step is marked absent, because “no such fact” is not something a clause can prove.

The check

eyeprolog --proof examples/context-schema-audit.pl > context-schema-audit.why.pl
eyeprolog --check-proof context-schema-audit.why.pl examples/context-schema-audit.pl

condition('C6', boundary_consistency, ok, 2).
obligation(absent, theory_scoped, \+ allowed_shape(gps, 2)).
obligation(absent, theory_scoped, \+ allowed_shape(tampered, 1)).
trusted(2).
verdict(checked_with_obligations).

Everything else replays, but the two absences are obligations: the proof is valid on condition that the schema is complete. C6 confirms that nothing in the program contradicts them. If someone forgot to list a legitimate shape, the audit would still pass the check, and the obligation lines say exactly where that assumption sits.

Try it

Add allowed_shape(gps, 2). and run again. Only the tampered violation remains, and its obligation is the only one left.
Add a third message whose context is the single field heartbeat and predict its shapes. Does context_member/2 still work when there is no comma at all?
Change the schema so that gps may have either 2 or 3 arguments. Which closed-world assumption have you just relaxed?

Learn more in The Art of EyeProlog, Chapters 9 and 12.

This site is open source. Improve this page.