Munksgaard / session-types

MIT License
549 stars 21 forks source link

Potential safety issue #8

Closed laumann closed 9 years ago

laumann commented 9 years ago

This just occured to me:

extern crate rust_sessions;

use std::thread::spawn;
use std::sync::mpsc::channel;

use rust_sessions::*;

type Proto = Send<u8, Eps>;

fn main() {
    let (tx, rx) = channel();
    let guard = spawn(|| {
        let c: Chan<(), Proto> = accept(tx).unwrap();
        c.send(42).close();
    });
    let c: Chan<(), Proto> = rx.recv().ok().unwrap(); // Does not use request!!
    c.send(42).close();
}

Compiles and fails in our current version:

target/debug/examples/fail 
target/debug/examples/fail 
thread '<main>' panicked at 'called `Result::unwrap()` on an `Err` value: "SendError(..)"', /home/laumann/rustc/src/libcore/result.rs:729

Arguably it is not using the API "fully correctly", but it still manages to obtain connected session-typed channels with incompatible types

tov commented 9 years ago

I wonder if having a different type for before connect/accept and after would work better.

laumann commented 9 years ago

I considered the same thing, something like

struct SessionSender<P>(Sender<Chan<(), P>>);   // Impl accept on this
struct SessionReceiver<P>(Receiver<Chan<(), P>>); // Impl request on this

fn init_session<P: HasDual>() -> (SessionSender<P>, SessionReceiver<P::Dual>) {
    let (tx, rx) = channel();
    (SessionSender(tx), SessionReceiver(unsafe { transmute(rx) }))
}

But I think the session_channel function does what we want. The crucial factors seems to be to (a) disallow manual construction of Chans and (b) ensure the entry points cannot produce two end-points with incompatible protocol types

Manishearth commented 9 years ago

Disallowing manual construction of chans is trivially easy with a lint :)

laumann commented 9 years ago

Can it be done now? Its fields are private...

Manishearth commented 9 years ago

We just want to disallow using the SessionSender()/SessionReceiver constructors and accept(..), right?

Manishearth commented 9 years ago

If marking them private will do it I don't mind.

Manishearth commented 9 years ago

I can write a lint if you just specify what patterns should be disallowed. (What sort of functions, and if you want you can specify specific types which should or should not be fed to them)

laumann commented 9 years ago

AFAIK having private fields disallows manual construction outside the defining crate

Manishearth commented 9 years ago

Yep.

laumann commented 9 years ago

I think that is enough then. As long as we control how Chans are constructed we should be able to ensure protocol consistency. But I wonder if there is another way...

Munksgaard commented 9 years ago

Otherwise we should just remove accept and request? Do we actually need them?

Munksgaard commented 9 years ago

@laumann and I have discussed this a bit. It seems that accept and request have their uses. Specifically, one might imagine a case where multiple clients need to be able to establish a session with a single server. Cloning a Sender to all the clients allows them to accept a session from the server.

I think #9 will be an adequate fix for this issue.