Live data from Hacker News

Translating All C to Rust (TRACTOR)

darpa.mil

291–300 of 403 posts

Re: Translating All C to Rust (TRACTOR)

#291

Earlier quoted context omitted.

You’re done editing the comment now? Do you think UB-as-feature is something that someone would honestly describe C or C++ as? It’s a pretty demeaning way of framing things. Indeed it’s a tongue-in-cheek remark, a vhimsical exaggeration/description of the by-default UB of those languages which was added to the end of the completely factual description of the role that finding UB in the Safe Rust subset of the standar…

> Do you think UB-as-feature is something that someone would honestly describe C or C++ as? Yes. That's how I describe it. That's also how Ralf Jung (long time Rust contributor and one of the main people behind Miri) describes UB in both Rust and C++ (although he says C++ overdoes it) [1] The thing I edited out of my comment was "motte and bailey fallacy" because after reflecting a bit I thought it was unfair. But no…

> Yes. That's how I describe it. That's also how Ralf Jung (long time Rust contributor and one of the main people behind Miri) describes UB in both Rust and C++ (although he says C++ overdoes it) [1]

Okay. Then I was wrong about that.

> The thing I edited out of my comment was "motte and bailey fallacy" because after reflecting a bit I thought it was unfair. But now you're actually trying to retroactively reframe as a joke.

What a coincidence. I had written on a post-it note that you were going to pull out an Internet Fallacy. (I guess it’s more about rhetoric.)

I guess you’ve never seen someone explain after the fact that they were being tongue in cheek (it’s not a joke, it’s an exaggeration)? Because jokes, sarcastic remarks are always clearly labelled and unambiguous? Okay then. I guess it was a Motte and Bailey.

Re: Translating All C to Rust (TRACTOR)

#292

Earlier quoted context omitted.

Calling Steve Klabnik (of all Core Rust background people, literally all of them) an “absolutist” proves how unreasonable you’re being.

Why do you feel it is unreasonable for this person to have human failings? What label would you find suitable?

You’re either reframing the statement to be about human failings overall—the lack thereof—or you’re assuming the conclusion.

Re: Translating All C to Rust (TRACTOR)

#293

Earlier quoted context omitted.

> have to imagine that in the general case it will be a translation to unsafe Rust, with occasional isolated leaf nodes being translated to safe Rust. That’s not what they are aiming for. FTA: “The goal is to achieve the same quality and style that a skilled Rust developer would produce” > just imagine how much harder it is to write automatic translation to borrow-checker-approved code that accounts for all the possi…

> undefined behavior gives the compiler leeway in deciding what a program does, so the more undefined behavior a C program invokes, the easier it is to translate its code to rust. That's the kind of language lawyer approach that caused a rebellion in the last decade amongst C programmers against irresponsible compiler optimizations. "Who cares if your program actually works as intended? My optimization is legal accor…

> I don't see any evidence that that's the attitude being taken by TRACTOR — I sure hope it isn't.

I don’t see any way it can do otherwise. As a simple example, what would one translate this C statement to:

  int i;
  …
  i = abs(i);
? I would expect TRACTOR to generate (assuming 64-bit integers):

  let i: i64;
  …
  i = abs(i);
However, that can panic in debug mode and return a negative number in release mode (https://doc.rust-lang.org/stable/std/primitive.i64.html#meth...), and there’s no way for TRACTOR to know whether that makes the program “work as intended”. That code may have worked fine/fine enough) for decades because its standard library returns zero for abs(INT_MIN).

Re: Translating All C to Rust (TRACTOR)

#294
post #159

Earlier quoted context omitted.

in this case it seems to me the hard task that DARPA has chosen is to get me to forget how much they spent on pushing Ada. You hate jumbo jets, high-speed trains, air traffic control, and satellites?

Do you know what fear is? Getting in an airplane where the flight controls use NPM.

I have enough fears about features in the entertainment system, and that performance options are accessed through that same touch screen UX.

Re: Translating All C to Rust (TRACTOR)

#295

Earlier quoted context omitted.

Apart from runtime/embedded requirements, there's the big question of how you represent what C is doing in other languages that don't have interior pointers and pointer casting. For example, in C I might have a `struct foo*` that aliases the 7th element of a `struct foo[]` array. How do you represent that in Java or Python? I don't think you can use regular objects or regular arrays/lists from either of those languag…

I’ve spent the past few months translating a C library heavy in pointer arithmetic to TypeScript. Concessions have to be made here and there but ended up making utility classes to capture some of the functionality. Structs can be represented as types since they are able to also to be expressed as unions similar to structs. These const types can have fields updated in place and inherit properties from other variables…

Very cool! Is your work all by hand, or have you been able to automate some of it?

Re: Translating All C to Rust (TRACTOR)

#296

Earlier quoted context omitted.

It'd require using unsafe code somewhere in the stack. Not necessarily by the mentee. It's possible that the AVX code wasn't properly hidden behind a safe abstraction in a library.

That still means the unsafe code is at fault.

Yes, but if a developer can't trust the abstractions then isolating unsafe code behind them is of no value.

Re: Translating All C to Rust (TRACTOR)

#297
post #288

Earlier quoted context omitted.

> The amount of people using stuff CBMC is like trying to boil the ocean. That's like saying, "Getting everyone to use Rust or TDD or X is like trying to boil the ocean." It's impossible to solve all things for all people at once. But, that doesn't mean that we can't advocate for tooling that can be used today to build safer software. This goes beyond C, as such tools and techniques are being ported to many languages…

50 years are more than enough time to improve C's security story.

Yep, but we have to deal with what we have. For better or for worse, C remains where it is. We can either use process and tools to improve existing C, or throw our hands up.

I prefer to work toward fixing what is. We are unlikely to see things like array slices in C, and even if such features were added, this does nothing to fix the billions of lines of legacy code out there.

Re: Translating All C to Rust (TRACTOR)

#298
post #287

Earlier quoted context omitted.

That's a rather cynical interpretation of these initiatives. CHERI, for instance, has been in development for twenty years. It predates the general availability of open source tools like CBMC or languages like Rust. But, that doesn't make the concept better or obsolete . It makes it complementary . Hardware security is complementary to software security. Mitigations at the hardware level, the hypervisor level, and th…

Complementary, as the ultimate defence wall. Many of the issues caused by C, are solved by Modula-2, Object Pascal and Ada, we didn't need to wait for Rust. But those aren't the languages that come for free with UNIX. Or even better, they would be solved by C itself, if WG 14 cared even a little about providing proper support for slices, proper arrays and proper string types, or even as library vocabulary types. But…

There is nothing wrong with defense in depth. But, this is not where things stop.

I make extensive use of bounded model checking in my C development. I also use privilege separation, serialization between separate processes, process isolation, and sandboxing. That's not because bounded model checking has somehow failed, but because humans are fallible. I can formally verify the code I write, but unless I'm running bare metal firmware, I also have to deal with an operating system and libraries that aren't under my direct control. These also have vulnerabilities.

That's not a trivial thing. The average software stack running on a server -- regardless of whether it is written in C, Rust, Modula-2, Pascal, Ada, or constructively proven Lean extracted to C++ -- still goes through tens of millions of lines of system software that is definitely NOT safe. All of that code is out of a developer's control for now. Admins can continually apply patches, but until those projects employ similar technology, they are themselves a risk.

One day, hopefully, all software and firmware will go through bounded model checking as a matter of course. Until then, we work with what we can, and we fix what we can. We can also rely on hardware mitigations where applicable. That's not failure as you have claimed, but practical reality.

Re: Translating All C to Rust (TRACTOR)

#299

This isn't some "pie in the sky" thing, Immunant has a working C to Rust transpiler and it's really interesting: https://github.com/immunant/c2rust

Their work was also previously sponsored by DARPA, though I do not know if it was under this program or something else.

It must have been a different program, as this one hasn’t started yet, but perhaps by another program by the same program manager.

Re: Translating All C to Rust (TRACTOR)

#300

Surely this could be better pitched to researchers as just another AI benchmark, a bit like ARC Prize? ;) There could be some exiting C projects that are already public, with tests for feedback during development iteration and some holdout tests, and some holdout projects too with a leaderboard and prizes. For preferences about converted code quality, both automated assesment and human preferences could be ranked wit…

And like with most other competition/benchmark, the result is likely optimizing for the benchmark and not the wider goal ;-). It’s difficult to get a serious effort without people trying to game the benchmark.
Post reply on HN