Beta
×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

SRI/Cambridge Opens CHERI Secure Processor Design

Unknown Lamer posted about 3 months ago | from the dreaming-of-hurd/coyotos dept.

Hardware Hacking 59

An anonymous reader writes with some exciting news from the world of processor design: Robert Watson at Cambridge (author of Capsicum) has written a blog post on SRI/Cambridge's recent open sourcing of the hardware and software for the DARPA-sponsored CHERI processor — including laser cutting directions for an FPGA-based tablet! Described in their paper The CHERI Capability Model: Reducing Risk in an age of RISC, CHERI is a 64-bit RISC processor able to boot and run FreeBSD and open-source applications, but has a Clang/LLVM-managed fine-grained, capability-based memory protection model within each UNIX process. Drawing on ideas from Capsicum, they also support fine-grained in-process sandboxing using capabilities. The conference talk was presented on a CHERI tablet running CheriBSD, with a video of the talk by student Jonathan Woodruff (slides).

Although based on the 64-bit MIPS ISA, the authors suggest that it would also be usable with other RISC ISAs such as RISC-V and ARMv8. The paper compares the approach with several other research approaches and Intel's forthcoming Memory Protection eXtensions (MPX) with favorable performance and stronger protection properties.
The processor "source code" (written in Bluespec Verilog) is available under a variant of the Apache license (modified for application to hardware). Update: 07/16 20:53 GMT by U L : If you have any questions about the project, regular Slashdot contributor TheRaven64 is one of the authors of the paper, and is answering questions.

cancel ×

59 comments

Sorry! There are no comments related to the filter you selected.

To make things more secure, make them simpler (1)

Anonymous Coward | about 3 months ago | (#47465725)

Complexity is bad for security.

Re:To make things more secure, make them simpler (1)

Tmackiller (959837) | about 3 months ago | (#47465783)

Agreed, the more complex something becomes, the more likely there is to be a blindspot or loophole in the design.

Re:To make things more secure, make them simpler (3, Informative)

Anonymous Coward | about 3 months ago | (#47465847)

Capabilities are simpler than "simple" paged memory management. Every pointer carries permissions, enforced in hardware, instead of requiring several layers of software to perform their own ownership management.

Re:To make things more secure, make them simpler (2)

TheRaven64 (641858) | about 3 months ago | (#47469389)

Note that, in our implementation, capabilities are orthogonal to paged memory management. CHERI's capabilities are within a virtual address space. The MMU is a really useful abstraction for an OS wanting to isolate processes from each other and implement things like swapping, lazy allocation, and so on. It's a pretty poor abstraction for implementing memory safety and sandboxing within an application. We regard the two as complementary: CHERI provides both a traditional MIPS TLB and capabilities, and the FreeBSD port uses them both.

Re:To make things more secure, make them simpler (1)

Anonymous Coward | about 3 months ago | (#47465957)

Complexity is bad for security.

To paraphrase Einstein, "security should be as simple as possible, but no simpler."

Re:To make things more secure, make them simpler (0)

Anonymous Coward | about 3 months ago | (#47466523)

Which is why file systems should go back to two access levels: root only and user only. All of those complex permissions are too complex, when it should be boiled down to a single bit. If it is good enough for RAM, it is good enough for hard disk.

Re: To make things more secure, make them simpler (0)

Anonymous Coward | about 3 months ago | (#47467665)

I'd share my 2 cents with you, but...

Re:To make things more secure, make them simpler (0)

Anonymous Coward | about 3 months ago | (#47466061)

It's a trade-off... things get more interesting and easy to use as they get more complex. An abacus is an unhackable computing device (well, at least if you don't consider hacking it with an axe), but you can't use it to see kitten pictures.

Re:To make things more secure, make them simpler (1)

Anonymous Coward | about 3 months ago | (#47466701)

Simplicity is an illusion we place on reality. In reality, simplicity is merely trading complexity for a predefined set of rules that only come about through even more complex ideas.

This is exactly what they are doing. They are trading the complexity of 5 million different programmers trying to be secure for hardware designed by a few really smart people.

In this case, things become simpler for everyone, including the hackers, as they only have to hack one model. However, since the compilers are in on it, they should be able to patch any security holes at the compiler level.

Then you have to worry about everyone affected recompiling, and ....

Oh, we're back here again.

Re:To make things more secure, make them simpler (3, Insightful)

TheRaven64 (641858) | about 3 months ago | (#47466749)

Yes, we agree. That's why we have a fairly simple set of instruction set extensions requiring no complex logic (TCAMs, associative structures, complex data structure walkers, and so on) that we have formally verified provide the required security properties.

Laser cutting directions! (4, Insightful)

Gollum (35049) | about 3 months ago | (#47465991)

Breathless excitement!

The achievements in the rest of this paper far outweigh the existence of a tablet built on this foundation.

They've created their own 64-bit processor! They've implemented a compiler for it! They've ported FreeBSD to it! That's some seriously impressive stuff!

But the leader has to be the laser cut tablet assembly. :-(

Re:Laser cutting directions! (0)

Anonymous Coward | about 3 months ago | (#47466069)

I'm surprised it's not called 3D printing. You know how every single manufacturing technique under the sun has been rebaptised as 3D printing...

Re:Laser cutting directions! (0)

Anonymous Coward | about 3 months ago | (#47466547)

It takes more effort to rebrand a subtractive process as 3d printing... like the machine in my shop that 3d prints air into solid blocks of aluminum using an end mill.

Re:Laser cutting directions! (1)

Impy the Impiuos Imp (442658) | about 3 months ago | (#47466685)

Hogging out a hole : to reverse-3D print

Re:Laser cutting directions! (1)

Garridan (597129) | about 3 months ago | (#47470289)

3d printing air into solid aluminum? I'm sold! Can you do transparent aluminum too?

Re:Laser cutting directions! (3, Informative)

TheRaven64 (641858) | about 3 months ago | (#47466733)

To be fair to the submitter, Theo did some amazing work with the laser cutter to produce the tablets. Mine doesn't have the SRI and Cambridge logos etched into the front (or a battery, actually - it's one of the first models) but the it's still very nice. Not really competitive with the iPad, but definitely something we can plausibly use as a prototype.

Re:Laser cutting directions! (0)

Anonymous Coward | about 3 months ago | (#47467215)

You clearly don't understand how exciting lasers are.
 
Ow, my eye!

Re:Laser cutting directions! (0)

Anonymous Coward | about 3 months ago | (#47467909)

FPGA-based tablet!

Fpablets are cool, leaving you breathless as your try to pronounce their name. Impressive is also the dare to implement a capability based model with some backing that could lead to consumer products eventually. How many decades this has been put to side now in the general market?

Re:Laser cutting directions! (2)

TheRaven64 (641858) | about 3 months ago | (#47468787)

Impressive is also the dare to implement a capability based model with some backing that could lead to consumer products eventually. How many decades this has been put to side now in the general market?

Most of the early capability systems (with the exception of the M-Machine from MIT) were extreme-CISC chips. They implemented complex capability walking so you could have multiple levels of indirection before you got to the . We aim to provide enough hardware support that you can implement these things in software, in a way that can't be bypassed. We're also aiming for a single hardware abstraction that scales from per-object bounds checking up to large sandboxes (think NaCl, but cheap and hardware-enforced).

The limitation of the M-Machine was that it required power-of-two sized objects, so you ended up with a huge amount of padding (very bad for caches, TLBs, and everything else).

In terms of consumer products... wait and see. We're exploring a few exploitation routes, but there's nothing concrete. Ask again in a year or two...

Re:Laser cutting directions! (0)

Anonymous Coward | about 3 months ago | (#47471637)

Wouldn't routers be a nice first target?

Limited software suite that needs adapting, I believe a lot of routers already use RISC processors and a real use for unbreakable security.

Re:Laser cutting directions! (1)

TheRaven64 (641858) | about 3 months ago | (#47473321)

A lot of routers actually run FreeBSD/MIPS. The FreeBSD MIPS port was jointly done by Juniper and Cisco. The CHERI project is jointly funded by two DARPA programs, CRASH and MRC. The MRC-focussed part is looking as software-defined networking and switch fabrics. Part of this includes putting CHERI on the NetFPGA 10G boards (which have 4 10GigE ports, so can do a reasonable amount of packet pushing). For a switch, you typically want some hardware acceleration of lookup tables for routing and so on, but CHERI might make sense for isolating flows from each other. We'll see over the next year...

Re:Laser cutting directions! (1)

Guy Harris (3803) | about 3 months ago | (#47487059)

Most of the early capability systems (with the exception of the M-Machine from MIT) were extreme-CISC chips.

Or CISC and extreme-CISC multi-chip processors, such as the Cambridge CAP computer [wikipedia.org] , the Plessey System 250 [wikipedia.org] , the Flex machine [wikipedia.org] , and the IBM System/38 [wikipedia.org] .

Looking To Buy Established Website ($50,000 - $5,0 (-1, Flamebait)

bizbroker (3751939) | about 3 months ago | (#47475051)

Dear Members, We are always thinking about buying high quality, established internet businesses and websites. We pay in cash between $50,000 - $5,000,000 (After proper Due Diligence) Fogged headlights we’re looking for: 1. Established Websites We’re looking to buy established websites, not “turnkey” sites. We are looking for an userbase and/or some reputation in the site’s niche. 2. Significant Traffic We have been looking for websites with significant traffic in their sector. GEO USA, UK, Europe, Russia and Australia 3. We like to Websites With premium keyword domains, home-based, relocatable, 100% automatic, E-Commerce, Drop Shipping, Ad Sales, AdSense, Advertising, Affiliate, Amazon, App Sales, ClickBank, Commission Junction, CPA, Dropship, In-App Sales, Infolinks, Sales, Services, Subscription, Logo Maker, PDF Creator, etc. 4. We Are Not Looking to Buy. - Internet sites with no organic search traffic - Grown-up sites “Me too” sites: proxies, arcades, etc. Contact us for additional information and for a free valuation of your business! BizBroker24.com Website Broker and E-Business Mergers & Acquisitions Phone: +1 (786) 350 1560

4chan comment (1, Offtopic)

bmo (77928) | about 3 months ago | (#47467203)

>CHERI processor

Really? Cheri?

http://cheri.com/ [cheri.com] You have been promoted!

NOT SAFE FOR WORK.

--
BMO

Re:4chan comment (1)

bmo (77928) | about 3 months ago | (#47467585)

I know it's poor form to bitch about moderation, but "offtopic?" Really?

It never crossed anyone's mind to type the name into a web browser? You know, just to make sure that it didn't link to something like lemonparty?

--
BMO

Re: 4chan comment (0)

Anonymous Coward | about 3 months ago | (#47467815)

Little boys have been "finding" dirty substitutions for acronyms ever since acronyms were invented.

Go back to 4chan. And take those darn cats with you!

Any questions? (4, Informative)

TheRaven64 (641858) | about 3 months ago | (#47468085)

I'm one of the authors of the paper (I did the LLVM support, some of the ISA design and the hardware implementation, and a token amount of OS work), so I'm happy to answer questions about it.

source code of the processor? But software patents (1)

raymorris (2726007) | about 3 months ago | (#47468743)

A processor is a piece of hardware, correct?
TFS says the Verilog source code of the processor is available. "Source code" sounds like software. I bet you can even run that source code on a general purpose CPU, can't you?

So is the processor hardware, software, or are the people who scream about "software patents" utterly clueless about computer engineering?

Re:source code of the processor? But software pate (5, Informative)

TheRaven64 (641858) | about 3 months ago | (#47468895)

The processor is implemented as a softcore in BlueSpec SystemVerilog, which is a high-level hardware description language (HDL). The source code can be compiled to C for simulation, so you can run it on a general-purpose CPU. We get around 30K instructions per second doing this. It can also be compiled to verilog and then synthesized into gate layouts for an FPGA. We can run at 100MHz (probably 125MHz, but we don't push it) in an Altera Stratix IV FPGA, with around 1 instruction per clock (a bit less), so around 3000 times faster than simulation.

In theory, you could also take the verilog and generate a custom chip. In practice, you wouldn't want to without some tweaking. For example, our TLB design is based on the assumption that TCAMs are very expensive but RAM is very cheap. This is true in an FPGA, but is completely untrue if you were fabbing a custom chip.

Although we use the term 'source code', it's perhaps better to think of it as the code for a program that produces a design of a processor, rather than the source code for a processor.

In terms of software patents, there's some annoying precedent that a software implementation of a architectural patent can be infringing. The MIPS architecture that we implement has LWR and LWL instructions that accelerate unaligned loads and stores. These were patented (the patents have now expired) and the owners of the patent won against someone who created a MIPS implementation where these two instructions caused illegal instruction traps and were emulated in software. The software implementations were found to infringe the hardware patent.

Re:source code of the processor? But software pate (1)

goarilla (908067) | about 3 months ago | (#47474001)

In terms of software patents, there's some annoying precedent that a software implementation of a architectural patent can be infringing. The MIPS architecture that we implement has LWR and LWL instructions that accelerate unaligned loads and stores. These were patented (the patents have now expired) and the owners of the patent won against someone who created a MIPS implementation where these two instructions caused illegal instruction traps and were emulated in software. The software implementations were found to infringe the hardware patent.

I have one of those in my home-router: a Lexra LX4189. It's a real shame though, such legal shenanigans didn't help the MIPS ISA overall.

Re: source code of the processor? But software pat (0)

Anonymous Coward | about 3 months ago | (#47468945)

Hardware description language is also code. In fact, I wrote most of this one. Woo hoo! I'm famous!
-Jon Woodruff

Re: source code of the processor? But software pat (0)

Anonymous Coward | about 3 months ago | (#47469907)

Wooooohoo!

Re:source code of the processor? But software pate (1)

angel'o'sphere (80593) | about 3 months ago | (#47468953)

The 'source code' we are talking about is not running on a processor.
It is written in a HDL, a 'hardware description language'. The compiler is generating a chip layout which is then burned into an FPGA, a 'field programmable gate array' (or was it 'free'?)
So they use a 'programming language' to describe the logic, the circuits, of the processor.
The final result ofc is hardware that is capable of running FreeBSD and user land applications.
Hope that helped ;)

How does it compare to Unisys MCP ? (0)

Anonymous Coward | about 3 months ago | (#47469131)

It appears Unisys does the fault isolation by means of memory-safe programming languages. Which do not necessarily need a GC.

At least that is my understanding.

Can you share your analysis on MCP and how it compares to your approach ?

Re:How does it compare to Unisys MCP ? (5, Informative)

TheRaven64 (641858) | about 3 months ago | (#47469335)

There's a little bit of comparison to the Burroughs architecture that was one of the forerunners of the Unisys architecture in the paper. I'm not overfly familiar with the later Unisys MCP, so this may be wrong:

Our approach was explicitly intended to work with language that are not memory safe (i.e. C and friends). If you have a memory-safe language, then there is some cost associated with enforcing the memory safety in software, which CHERI can assist with, but you don't see much of a win.

As soon as you start mixing languages, you get the worst of all worlds. A typical Android application is written in C and Java (and some other things) and so gets all of the memory safety of C, plus all of the performance of Java. A single pointer error in the C code can corrupt the Java heap. One of my students last year implemented a modified JNI on CHERI that allows this sort of mixing but without the disadvantages. Java references are passed to C code as sealed capabilities, so the C code can pass them back to the JVM, but can't dereference them. The C code itself runs in a sandbox (C0 - the capability register that identifies the region of memory that normal MIPS loads and stores can use - is restricted to a smallish subset of the total [virtual] address space) so any pointer errors inside the C are constrained to only touch the C heap (of that particular sandbox - there can be a lot). He demonstrated running buggy and known-exploitable code in the JNI, without it compromising the Java code, with a very small overhead for calling in and out of the sandbox. Most interestingly, he was also able to enforce the Java security model for native code: the sandboxed code couldn't make system calls directly and had to call back into the currently active Java security monitor to determine whether it was allowed to.

Another of my students implemented an accurate (copying, generational) garbage collector for capabilities. This can be used with C code, as long as the allocator is outside of the normal C0-defined address space (otherwise pointers can leak as integers into other variables and be reconstructed). In particular, you can use this to track references to high-level language objects as they flow around C code and either invalidate them or treat them as GC roots, so you don't get dangling pointer errors. Or you can just use his allocator in C and have fully GC'd C code...

My understanding of MCP is that it uses high-level languages in the kernel, but does nothing to protect (for example) typesafe ALGOL code from buggy C code within the same userspace process.

Re:How does it compare to Unisys MCP ? (0)

Anonymous Coward | about 3 months ago | (#47469503)

Is the overhead of memory-safe ALGOL really that bad ? Isn't it the use of C which we should question ? After all, Fortran leads in efficiency, without all those dirty low-level techniques.My understanding is that Fortran code can be made memory-safe with very little effort.

Re:How does it compare to Unisys MCP ? (4, Informative)

TheRaven64 (641858) | about 3 months ago | (#47469591)

Currently, Ohloh.net is aware of around 11 billion lines of C/C++ code. I'm including C++ because, while it's possible to write memory-safe C++, all of the evil pointer tricks that are permitted in C are also allowed in C++. Rewriting 11 billion lines of code, even in a language that is 100 times more expressive than C, would be a daunting task. Note that Ohloh only tracks open source code in public repositories: there's a lot more that's in private codebases.

For a fully memory-safe language, you need things like bounds checks on array accesses. Some research from IBM about 10 years ago showed that, with JVMs of the time, the cost of bounds checks accounted for the vast majority of the difference in performance between C++ and Java implementations of the same algorithms. They did some nice work on abstractions that allowed most bounds checks to be statically elided, but their approach never made it into the language. The overhead is somewhat hidden by superscalar architectures (the bounds check is done in parallel and the branch is predicted not-taken), but not on low-power in-order chips like the Cortex A7 that you'll find in a lot of modern mobile phones.

Re:How does it compare to Unisys MCP ? (0)

Anonymous Coward | about 3 months ago | (#47469765)

I appreciate your comments, but would like to add that it appears to me that correctness+security has by now become more important for applied computer science than processing throughput.

Users are starting to question IT security in general. Which is obviously a kind of "damocles sword" hanging over the profession.

Re:How does it compare to Unisys MCP ? (4, Informative)

TheRaven64 (641858) | about 3 months ago | (#47469899)

I appreciate your comments, but would like to add that it appears to me that correctness+security has by now become more important for applied computer science than processing throughput.

Yes, that's one of the motivations for our work. Now seems to be the time when it's possible to persuade CPU vendors that dedicating a little bit more hardware to security is valuable. It isn't quite the dichotomy that you describe though, because you can either implement security features in software or hardware and doing so in hardware can mean that you see a performance improvement for the sorts of use cases that people increasingly care about.

Re:How does it compare to Unisys MCP ? (0)

Anonymous Coward | about 2 months ago | (#47500465)

www.tekmuzik.com

You sure about this statement of yours man? apk (-1)

Anonymous Coward | about 3 months ago | (#47470391)

"A typical Android application is written in C and Java (and some other things) and so gets all of the memory safety of C, plus all of the performance of Java." - by TheRaven64 (641858) on Wednesday July 16, 2014 @03:21PM (#47469335)

You might want to REVISE & REVERSE that statement (hope your work isn't as "back-asswards" on that CPU too).

APK

P.S.=> Since that IS, most DEFINITELY, in reverse from you - no questions asked... apk

Addendum: It's that, or you have... apk (-1)

Anonymous Coward | about 3 months ago | (#47470411)

One hell of a weird sense of humor (were you ribbing on Android apps?) - Don't blame you IF you were picking on them either (Android, yes a Linux, with a STUPID java/dalvik front end user interface no less) - they're being torn up daily on the security front!

APK

P.S.=> I'm referring to what I quoted from you here http://hardware.slashdot.org/c... [slashdot.org] since I suspect STRONGLY, that you're BETTER than that (& were being facetious)... apk

Re:How does it compare to Unisys MCP ? (1)

weav (158099) | about 3 months ago | (#47477325)

Coming late to this party, I can only share this one datapoint: If I recollect right, it was the hardware on the Burroughs Large Systems that was memory-safe. Arrays were done as Segment Descriptors, and if you indexed outside the segment it raised an exception. Byte-addressed (for 6-bit, 8-bit, etc bytes) were done as "String Descriptors" that referred to the Segment Descriptor.

The only other hardware I know of that did this lately was the UCSB P-system; there may be others since then.

Re:How does it compare to Unisys MCP ? (1)

TheRaven64 (641858) | about 3 months ago | (#47481157)

Yup. Compiling for the Burroughs architecture was easier than many segment-based systems, because they allowed segment descriptors to be placed in main memory, with the CPU responsible for tracking the value type by updating a tag. We adapt this slightly so that we only require one tag bit per 256 bits of main memory (the paper describes the implementation of this in some detail, but I'm happy to answer questions) to be able to safely store capabilities in main memory. Our design also allows normal C data structures to work as expected. You can mix C code compiled for MIPS and C code compiled for CHERI in the same binary (though you only get coarse-grained protection in the MIPS code).

The Burroughs architecture had very little impact on the computer architecture community, but was enormously influential in the design of VMs for high-level languages. One of our goals is to pull out the aspects of such VMs that are required for memory protection and put them back in the hardware, so a buggy VM has a far more limited security impact. My student's work on JNI dramatically reduced the amount of C code in the trusted computing base for the JVM implementation that he used.

Re:Any questions? (0)

Anonymous Coward | about 3 months ago | (#47469213)

I find very interesting what you have done and the presentation (video) too. I don't really have any questions but wish these kind of features would catch wind so much in that we at some, hopefully not too far, future would get these to commercially supported platforms. Great work and I wish you luck with your future work on it.

Re:Any questions? (4, Informative)

TheRaven64 (641858) | about 3 months ago | (#47469365)

We hope so too. One of the things on my short-term todo list is define a set of requirements for our extensions to C so that we can have source compatibility across different CPUs implementing similar ISA extensions. Of course, this is (optimistically) assuming that other CPUs are going to provide similar extensions...

Look this gifthorse in the mouth (1)

Garridan (597129) | about 3 months ago | (#47470187)

When old enemies arrive at your door bearing a gift horse large enough to fit a fireteam, don't stop at it's mouth, do a full cavity search.

Are there independent third-party audits underway? If DARPA likes it, I'm suspicious.

Re:Look this gifthorse in the mouth (1)

TheRaven64 (641858) | about 3 months ago | (#47473343)

I hope no one misses the irony of using a DARPA-funded network protocol to post about how evil DARPA is...

Re:Look this gifthorse in the mouth (1)

Garridan (597129) | about 3 months ago | (#47477517)

I didn't say that DARPA was evil. I just said that this merits an independent audit. I take your flippant answer for a "no".

Re:Look this gifthorse in the mouth (1)

TheRaven64 (641858) | about 3 months ago | (#47481135)

The flippant answer is all that your paranoia deserves. The work was undertaken by SRI and The University of Cambridge. The funding was provided by DARPA, but that's the extent of their involvement (other than creating a program with the goal of being able to redesign any aspect of computing with security in mind).

The code is no more or less meriting an independent audit than any other open source code. Less, actually, because we don't anticipate anyone actually using our open source reference implementation in production, we hope that CPU vendors will take the ISA extensions and apply them to their own chips, but we expect that (if they do) they'll do independent reimplementations. At the ISA levels, we have PVS / SAL proofs that we'll be publishing soon that the ISA does provide the desired security properties and you're welcome to audit those too.

Re:Look this gifthorse in the mouth (2)

Garridan (597129) | about 3 months ago | (#47484455)

The flippant answer is all that your paranoia deserves.

A healthy amount of paranoia is a must in the security industry. Every piece of security hardware or sofware demands third-party evaluation, even that made by people you trust completely. Not all flaws are deliberate. Thank you for your time, and (at last) thoughtful response.

Re:Any questions? (1)

complete loony (663508) | about 3 months ago | (#47471819)

Has anyone on the project thought about extending the design to include secure key storage? (I'm thinking specifically of something like TRESOR / TreVisor)

Re:Any questions? (0)

Anonymous Coward | about 3 months ago | (#47472733)

All you really need is 256 bits of fast register with that gets hard-zeroized on RESET, or hardware traps such as lost power. After that, you can encrypt all secure data in RAM with a secure stream cipher like ChaCha20 (or AES-CTR) using the address as the counter. Bam.

This is an interesting design. Have you thought about maybe posting seL4 to it once that's open-sourced in a couple of weeks? /akr

Re:Any questions? (1)

TheRaven64 (641858) | about 3 months ago | (#47473411)

This is an interesting design. Have you thought about maybe posting seL4 to it once that's open-sourced in a couple of weeks? /akr

Yes, we're looking forward to the seL4 release. Somewhat cautiously, as there's no mention of a license (if it's GPL'd, we probably won't put any effort into it). In CHERI, we have store-capability and load-capability permissions on both capabilities and pages. To implement the seL4 model (where capabilities are stored in special pages), we'd only need to use the TLB-grandularity protections, but it would be more interesting to provide fine-grained capability storage, which would reduce a bit of the difficulty in programming for seL4.

We're also interested in the impact on the proofs in seL4. For example, seL4 currently assumes that the TLB is correct as an axiom (read the errata sheet for any production CPU to see how valid that is). With CHERI, we have some proofs extending down into the ISA and into the implementation and it would be interesting to see how these could be coupled to have a proven-secure systems. The folks at UT Austin and Centaur are (independently of us, but we talk to them periodically) working hard on proving that properties of higher-level HDLs are mapped correctly to gate layouts, so in a few years it may be possible to have a microkernel with security properties proven correct right down to the gate level.

Ilya Bakulin is currently working on porting FreeBSD to run atop L4 and is interested in extending this port to run on seL4. That would also be an interesting approach when combined with CHERI, allowing a full FreeBSD to run with some critical services moved out and into a tiny TCB.

Re:Any questions? (1)

TheRaven64 (641858) | about 3 months ago | (#47473365)

We haven't specifically looked at key storage, but we are looking at potential ways of extending the approach to heterogeneous multicore systems, so that access to main memory could be delegated to accelerators (at varying levels of coupling) via capabilities and capabilities could be used to mediate access to accelerators. In this scheme, it would be possible to provide an encryption coprocessor that would store keys internally and perform encryption and decryption operations on blocks of memory delegated to it from userspace.

This is part of a more general problem, which is that most accelerator designs currently follow the model of a device, which requires kernel mediation to use and don't really support virtualisation well. The design you want is a resource that's cheap to access from userspace and easy to multiplex. Once you have that, it's easy to have useful crypto coprocessors (i.e. ones that cause a speedup for everything, rather than a slowdown for anything smaller than a few tens of KBs).

Re:Any questions? (1)

smallfries (601545) | about 3 months ago | (#47473349)

Is the code for the LLVM support publically available / do you have a link for it?

Re:Any questions? (2)

TheRaven64 (641858) | about 3 months ago | (#47473445)

Yup, it's on GitHub in two repositories, one for LLVM [github.com] and one for clang [github.com] . We've been pushing the fixes for MIPS IV upstream, but there are some changes to the mid-level optimisers to make them aware that not all pointers are integers and some extensions to the platform-independent code generators for the same.

We've upstreamed all of the FreeBSD changes required for the base processor (BERI) and the development boards, so FreeBSD 10 will run out of the box on CHERI (it just won't expose any of the capability features). The CHERI-enabled version of FreeBSD is also on GitHub [github.com] .

The code for the processor is just in a tarball at the moment. We're going to move it to some sensible public revision control system once we've worked out how much of our internal svn history wants to be included in the public release.

Acronyms with multiple meanings (1)

Damian J Pound (3635341) | about 3 months ago | (#47472779)

Multi-Pointer X, also called MPX

But does it... (0)

Anonymous Coward | about 3 months ago | (#47473981)

play Cheri Cheri Lady at startup?

Check for New Comments
Slashdot Login

Need an Account?

Forgot your password?