require/typed doesn't protect with contract properly

[sorawee]

What version of Racket are you using?

8.5 [cs]

What program did you run?

#lang racket

(module a typed/racket
  (provide f)
  (: f (-> Byte Integer))
  (define (f x)
    (add1 x)))

(module b typed/racket
  (require/typed (submod ".." a)
                 [f (-> Byte Integer)])
  (provide f))

(require 'b)

(f "a")

What should have happened?

A contract error, saying that "a" is not a number.

If you got an error message, please include it here.

f: broke its own contract
  promised: exact-integer?
  produced: #<garbage>
  in: (-> any/c exact-integer?)
  contract from: (interface for f)
  blaming: (interface for f)
   (assuming the contract is correct)

In DrRacket, running the program repeatedly and quickly will crash DrRacket.

EDITED:

Here's another fun example:

#lang racket

(module a typed/racket
  (provide f)
  (: f (-> Byte Byte Integer))
  (define (f x y)
    (+ x y)))

(module b typed/racket
  (require/typed (submod ".." a)
                 [f Any])
  (provide f))

(require 'b)

(define a "abcdefghijk")
(define b "my-password")

(f a 8)

returns "my-password" pretty reliably in non-sandbox mode.

[capfredf]

In DrRacket, running the program repeatedly and quickly will crash DrRacket.

This is surprising. cc @rfindler

[capfredf]

@sorawee I can't reproduce a crash on Linux with 8.5 cs

[samth]

The #<garbage> suggests that we're causing memory unsafety, so DrRacket crashing is Typed Racket's fault.

[samth]

I also get #<garbage> in the error on my HEAD linux version, with CS, so this bug is definitely real.

[capfredf]

Yeah, I get #<garbage> as well. I just thought DrRacket had some kind of isolation between it and programs it ran

[samth]

Ok, I think this is a simple miscommunication between the modules. a thinks that it's providing f to a typed module, so it doesn't need a contract. b thinks that it doesn't need to check the domain of f in require/typed because b is typed, and that it doesn't need to add protection to f when providing it because it doesn't define it locally.

Each of those decisions is sensible locally, but they don't all work together.

[bennn]

So, should b add protection when providing?

In general: require/typed imports from a typed module get full contracts.

[rfindler]

It does, but bugs like this are defeating that isolation. The isolation is in the language, not at the OS layer.

On Fri, Jul 8, 2022 at 9:04 AM Fred Fu @.***> wrote:

Yeah, I get # as well. I just thought DrRacket had some kind of isolation between it and programs it ran

— Reply to this email directly, view it on GitHub https://github.com/racket/typed-racket/issues/1256#issuecomment-1179027594, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADBNMBXLAZ56WGRN4QXQWLVTAYP3ANCNFSM52752EUQ . You are receiving this because you were mentioned.Message ID: @.***>

[samth]

@bennn Yes, I agree (basically we should just make require/typed not be a typed context).