differential-datalog icon indicating copy to clipboard operation
differential-datalog copied to clipboard

Fix unsoundness in DDValue traits

Open Kixiron opened this issue 3 years ago • 4 comments

The implementations of PartialEq, PartialOrd and PartialOrd for DDValue (seen here) are unsound since they allow what's essentially transmuting types into the incorrect type and using them with an innocuous == or < call. To fix this the trait implementations should have checks added to them and new *_unchecked() methods (eg. .partial_eq_unchecked()) should be added and used within generated code, since generated code statically knows the types of things that will be compared against each other (still with the debug_assert!()s for posterity's sake)

Kixiron avatar Dec 10 '20 18:12 Kixiron

Problem is, these traits are used internally by DD, which cannot be told to use our custom methods instead.

ryzhyk avatar Dec 10 '20 18:12 ryzhyk

That is very unfortunate and complicates things significantly. Do you think we could at least push the unsoundness back a level (and hopefully out of the range of normal users) by directly implementing the exposed DD traits such as PartialOrder?

Kixiron avatar Dec 10 '20 19:12 Kixiron

Not sure I understand. Any value passed to DD must implement Ord, and hence PartialOrd and Eq: https://docs.rs/differential-dataflow/0.11.0/differential_dataflow/trait.Data.html

There's probably a way to add another wrapper around DDValue with unsafe implementation of Ord and make sure that we strip this wrapper before returning the value to the user. Or we could go in the other direction and add a safe wrapper around unsafe DDValue.

ryzhyk avatar Dec 10 '20 19:12 ryzhyk

I have a partial solution that allows users to be checked and internals not to be

// This is what is currently DDValue would become
struct DDValueInner {
    ...
}

#[repr(transparent)] // Allows soundly transmuting between a `DDValue<Checked>` and `DDValue<Unchecked>`
pub struct DDValue<C: DDlogChecked = Checked>(
    DDValue,
    PhantomData<C>,
);

impl PartialEq for DDValue<Checked> {
    fn eq(&self, other: &Other) -> bool {
        if self.type_id() == other.type_id() {
            ...
        } else {
            panic!();
        }
    }
}

impl PartialEq for DDValue<Unchecked> {
    fn eq(&self, other: &Other) -> bool {
        ...
    }
}

pub struct Checked;
pub struct Unchecked;

mod sealed {
    use super::{Checked, Unchecked};

    pub trait DDlogChecked {}

    impl DDlogChecked for Checked {}
    impl DDlogChecked for Unchecked {}
}

Then we make our user-facing apis return DDValue<Checked> and internally DDValue<Unchecked>s are moved around, used and stored

Kixiron avatar Dec 10 '20 19:12 Kixiron