The gaps are closing for RISC-V. This is something I never thought would be possible. We might actually be able to buy fast RISC-V SoC in the next 10 years (fast == comparable speed with more modern ARM processors, such as i.MX6).
We need now other peripherals open sourced, such as SSD/USB/SATA/Audio/Keyboard/Mouse/embedded DisplayPort microcontrollers. Also network interface controllers.
Current 'all-in-one' projects are TERES from Olimex and MNT Reform.
I think people should prepare this 'shell' for when RISC-V comes once for all.
One big security fault I think we should solve is the compilers. Oeuf, Compcert and CakeML try to solve it, but there's the issue of bootstrapping. What code first generated the compiler? Who is watching the watchers?
http://oeuf.uwplse.org/ http://bootstrappable.org/
Other issue is hardware implants/trojans. OneSpin did some work on this, it seems. Optical inspection might be the answer. This paper also shows some progress (SIMCom):
https://arxiv.org/abs/1901.07299
Other issue is supply-chain attacks.
Unfortunately we can't control all variables, unless you're the military doing some highly-secure confidential processors.
>>4973 The compiler bootstrapping problem could be solved by using a hex editor to write a minimal assembler from machine code, and use that assembler to write a compiler.
What if the OS does something to the code? Or the microcode? I'm not in that level of paranoia, but it's important to think about these possibilities when designs a secure machine.
>>4975 I think essentially for machine to be as secure AND fast as possible, the following parts of the computational complex must be developed independently from other players by a trusted party:
a) ISA
b) Microarchitecture (the actual silicon chip or whatever)
c) Operating System
d) Compiler for the language to write the OS
I'm saying this because those four parts in fact have interdependencies between each other. Microarch will depend on the ISA, that much is obvious. ISA is developed with needs of the OS in mind. OS design will be highly influenced by the language that main components of the system are written in, as well as by the ISA of the machine. The language design will in turn depend on the ISA, and the design of the language and compiler itself will influence the software installing/writing procedures, including OS components.
So, I see at least one circular dependency here: ISA -> language -> OS -> ISA, and there are probably more subtle dependencies out there but I don't see them since I am not a pro and this post is made in attempt to outline the problem of trusted computational complex.
As for compiler bootstrapping, it looks like a meme. I mean, first, it's not new. Compiler bootstrapping is exactly the technique for writing a subset of language in the machine code (or the assembly, if we already have the assembler), then compiling a wider subset of language, and repeating this process until the full-featured compiler is compiled. Kinda extended to this, if we compile the compiler and get the same compiler, it is a good indication that we did good, but there is no indication if this compiler wasn't backdoored/bugged in the first place, and if you care about hardware cheating on you somehow, you have to do better than classic programming language, I believe, and it's gonna to be slow.
Like, from the top of my head, to ensure the region of memory is written correctly, we could use three different methods to write to three different places, then read from them via three different methods respectively (methods for r/w might ne incompatible if we do some weird stuff like writing to some separate bits) and make a decision on what is correct based on the majority vote (3v0, 2v1). It is retarded and slow, but it adds some possibilities for the machine to find out if something is corrupted or shit.
But this will not help with any active backdoors with their own firmware anyway, or with trojans from some other binaries you may want to run, so whatever guys. As I said, the whole complex is necessary. It seems that RISC-V might do the important job of being the ISA, so we have that at least.
>>4976 >As for compiler bootstrapping, it looks like a meme.
I'm not sure if I agree with you. I'm not only talking about backdoors (such as the Ken Thompson thesis), but also about possible bugs introduted by this chain of compilers.
For example: CompCert is meant to solve these bugs. But if you try to compiler CompCert, it requires OCaml and Coq. If you go to the page of OPAM they say you need GNU Make to compile it:
https://github.com/ocaml/opam/#compiling-without-ocaml
So, if any bug is introduced by GNU Make, all this chain might be compromised.
This is one of the issue DeepSpec is trying to solve, but I'm not sure they succeded (yet):
https://deepspec.org/
According to Data61, the seL4 project has proofs down to assembler. This means they analysed the binary code? How is that analysed? The these tools used be trusted?
>some military reads this thead and builds a new Kryptos sculpture, but this time with the initial compiler binary in it
>>4994 >I'm not sure if I agree with you.
I don't see you disagreeing with me.
Look:
1) compiler developer introduces a bug
2) that bug doesn't get detected on the bootstrap build, because it is obscure enough
3) that bug doesn't get covered by whatever tests the developers supply
4) ????
5) We have a BUG that your scheme doesn't do SHIT about!
>This means they analysed the binary code? How is that analysed? The these tools used be trusted?
I always scratch my head when somebody says they have "proven" code to work. I mean, some work at this field is probably useful to reduce the number of bugs from say 1% to 0.1% per LOC, but dude, computers are garbage. The memory cells fuck up, the disk I/O fucks up, the OS fuck up and the whole situation looks pretty grim if you ask me. And then I see some CompSci student with rainbows in the eyes dreaming about how he would prove that algorithm works. Well, algorithm might, but your program has 1000 and 1 way to shit itself.
But ultimately, yeah, if our model of the machine is correct enough, we can mathematically prove that some shit converts into some other shit and switches relevant states accordingly. Well, I cannot do it, because I suck, but all these type-0,1,2,3 grammars have to mean something.
>>4996 >I don't see you disagreeing with me.
Fair enough. I meant that I don't think this is a "meme", as you previously said. I think this is a important question to ask when making a high-assurance computer. And since RISC-V is basically re-doing the basis of computers (ISA), we might as well raise foundational questions like this one about compilers.
>The memory cells fuck up, the disk I/O fucks up [...]
Yep. But, to be fair, there is some research on this area too:
https://en.wikipedia.org/wiki/Fault_injection >Halting problem
I'm too dumb to understand this completely. But, if we get into the epistemology and meta-mathematics we can see some very fucked up issues, such as the Neurathian bootstrap, Ship of Theseus, Agrippa's Trilemma and so on:
https://en.wikipedia.org/wiki/Neurathian_bootstrap https://en.wikipedia.org/wiki/Ship_of_Theseus https://en.wikipedia.org/wiki/M%C3%BCnchhausen_trilemma
I'm not a specialist on any of this (very far from it, I'm just a useless NEET), but I was reading some articles on Willard Von Orman Quine and had this idea that a merge between Intuitionist Logic and Temporal Logic might open to more possibilities. The proof assistant Coq already uses Intuitionistic logic, so why not add a temporal domain, just like TLA+ did?
>>4996 It depends on the proof. Proofs prove a property of a system is true given some initial assumptions. Proofs for distributed systems often include the fact that machines or disks can fail. For other things they might add an assumption that disks won't fail, that you have an infinite amount of memory, or something else to that affect.
For actually doing the proofs, it will usually be done through bruteforcing through the state space, using a SAT solver, or requiring a person to construct the proof manually.
>The halting problem
Do note that this only applies to Turing complete languages. If you sacrifice Turing completeness you can have proofs that your program will indeed halt. See https://en.wikipedia.org/wiki/Total_functional_programming >>4997 Fault injection is not about proofs. It's still a verification technique, but it is much more a type of test. The keyword you are looking for is fault tolerance.
Like, obviously we won't piss away the useful works of mathematicians, but it ultimately shows that maths takes a model of reality assumed to be true, which is not always the case. Their work helps us within that model though.
>>4998 >Do note that this only applies to Turing complete languages.
Apparently, even MOV instruction in x86 is Turing complete, meaning that it is indeed Dark Ages RN.
>>4998 >Fault injection is not about proofs.
I never said it was. I meant that you can inject faults in the hardware and analyse how software reacts. From the same page linked:
>"This type of fault injection is called Hardware Implemented Fault Injection (HWIFI) and attempts to simulate hardware failures within a system."
>>5000 >maths takes a model of reality assumed to be true
Yep. Called Laws of Thought:
https://en.wikipedia.org/wiki/Law_of_thought
This presentation from Ian Hacking explores a bit this:
http://axqzx4s6s54s32yentfqojs3x5i7faxza6xo3ehd4bzzsg2ii4fv2iid.onion/watch?v=ZE94nNB2WOc >>5003 >meaning that it is indeed Dark Ages RN.
Too dramatic. There is still possibility to formal proof in many domains. As I said in OP, many companies are doing this kind of work today, in particular Bluespec, Data61, OneSpin and Galois.
>>5000 >it ultimately shows that maths takes a model of reality assumed to be true, which is not always the case
Mathematics does not have to do with reality, nor does it try to model it. Mathematics is always true though. There may be people who make a mistake in a proof and think they have shown something to be true which or may not be, but that doesn't reflect the true nature of mathematics.
>proving some faults in the code is very hard
Take something like memory safety. You can provably write memory safe programs in many modern languages. There are also many languages which offer safety against crashes. Most of the time these properties rely on the compiler / virtual machine being implemented correctly though. Type systems are also good for proofs. If your type system has refinement types you can even have proofs that your program will never preform a division by 0 operation. If your type system has dependent types, you can prove that every time you read from an array, you are reading within the array's bounds and not outside of it.
>>5003 I'm not sure what your point is. Practically all CPUs are turing complete. That doesn't mean you can't write programs which are guaranteed to halt on them. In fact it's quite trivial. For example take a UNIX weenies favorite simple program, Hello World. It is trivial to create an informal proof that the program will always halt especially since the control flow is entirely linear.
>>5008 >Mathematics does not have to do with reality, nor does it try to model it.
Yes it does. This is what a axiom is, a set of rules to explain a phenomena.
>Mathematics is always true though.
No, it's not. The other anon just linked the Godel's work. See also the work of Kripke and Dummett:
https://en.wikipedia.org/wiki/Saul_Kripke https://en.wikipedia.org/wiki/Michael_Dummett
We are not saying mathematics is useless. Very far from it. Mathematics build the technology we have today and it is the reason I'm able to send this message to you.
But, to use more buzzwords, we take the position of Instrumentalism, since the Foudationism is (probably?) impossible:
https://en.wikipedia.org/wiki/Instrumentalism https://en.wikipedia.org/wiki/Foundationalism
I thought about this for a long time. I came up with three or two fundamental questions, but thinking too much about this makes get into a near-psychotic mindset.
ps: I know this post has too many buzzwords, but hopefully you will read about all of them.
>>5008 >I'm not sure what your point is.
I'm not sure either, but doesn't it mean using MOV makes you use Thuring complete language by proxy. Like, using just one MOV already fucks you. There is no proof MOV finishes correctly.
Though the halting problem itself doesn't mean that we cannot prove some subset of programs.
>If your type system has
Well, there is a lot of languages like that, but they are not Haskell-tier or whatever.
>For example take a UNIX weenies favorite simple program, Hello World.
It's funny because recently I found out that halting a program in the OS might be just easier.
I took "int _start(){return 0;}" and tried to link an executable without C lib (gcc -c hello.c; ld -o hello hello.o). Guess what? This shit segfaults! Why? Because that return pops 0x1 from the stack into IP, and we have absolutely legit segfault. Now, imagine what could happen in less safe place. So, the only way to exit a program on loonix at least is to use the EXIT SYSTEM CALL. I was able to add a manual syscall before ret in the assembly listing, and it worked as expected, go figure.
>especially since the control flow is entirely linear
BTW if you use printf it parses your format string and file I/O isn't as simple as it looks, so I don't know how linear that shit is.
>>5025 >Ara achieves up to 67 DP-GFLOPS/W under the same conditions, which is 56% higher than similar vector processors found in literature.
I wonder if the idea of >>5006 would improve this even further...
>>5009 >an axiom is a set of rules to explain a phenomena
Axioms have nothing to do with explaining a phenomena. Axioms are about creating an initial set of truth of which you can create a logical framework on top of.
>Mathematics is not always true
Can you be more specific in what you mean? Just because you may need different systems of logic in order to cover all of the different things in mathematics, it doesn't mean it is false.
>mathematics is an abstraction from reality
This is more of a philosophical question of what mathematics abstracts. Mathematics has nothing to do with reality though. Mathematics is not based off of reality or physics. If reality was destroyed, mathematics would still remain. If physics got turn on its end, mathematics would remain the same.
>>5015 >using just one MOV already fucks you
I probably should have corrected you earlier, but MOV isn't actually Turing complete. What you are referring to is a series of MOV instructions followed by a JMP instruction back to the start of the program. It's more of a statement of how many different variants of MOV exists. Even though they may use the same mnemonic, they aren't actually the same instruction. Also using something which is capable of being Turing complete doesn't make you not. In this case if you were trying to prove if your program halted, you would need to prove that this construct did in fact terminate. For example recursion allows you to loop forever. However if you require that one of the arguments always gets structurally smaller each iteration it will be guaranteed to terminate. This is because you will eventually hit the lower bound of 0 where you can not make that argument any smaller.
>Haskell-tier
Haskell doesn't even have stuff like refinement types, dependent types, quantitative types, etc.
>halting a program in the OS might be just easier
The Halting Problem is not about the ability to halt, but rather proving a property of the program, specifically that it terminates in finite time.
>printf does not have linear control flow
I wasn't necessarily talking about a specific language or implementation, but specifically the idea. You can write a hello world program which has no loops all the way down to assembly.
>>5028 >Axioms are about creating an initial set of truth of which you can create a logical framework on top of.
This "set of truth" is based on what specifically? Logics. And then, logics is based on physics (ontology, mostly). Humans cannot quantify metaphysics, because it doesn't exist or we can't measure it. Mathematics "play" with physics to make deductions or inductions. It can create abstractions not directly related to physics, but in the end it all comes to a small 'set' of physical laws (commonly called "Laws of Thought").
>Can you be more specific in what you mean?
There is fundamental issues mathematics can't solve. I've linked many on >>4997 , please read through them.
>>5034 Ontology is not physics though, it is philosophy.
Just because mathematics can not solve every problem, it does not mean that there exists a contradiction in mathematics. It's like saying computers do not work since you can not solve the halting problem.
>>5028 >it doesn't mean it is false.
>Mathematics has nothing to do with reality though.
Well, if it has nothing to do with reality, it isn't true at all. I mean, I couldn't ever think of some other definition of "truth" than "happens in reality".
Personally, I connect it with hypotheses and their applicability limits. They are true somewhat, but we don't know everything.
Ultimately there is not much sense in talking about this, as this will not change certain power maths/science has.
In other words: of course mathematics has a connection to reality.
>I probably should have corrected you earlier, but MOV isn't actually Turing complete.
MOV probably is TC, specific command in machine code isn't, though I dunno how that loops plays into that. I think it can be removed for each specific program, or we can move code itself with MOV, avoiding the loop.
>In this case if you were trying to prove if your program halted, you would need to prove that this construct did in fact terminate.
This is most probably true.
Anyway enough of the halting problem, it is one of many.
>For example recursion allows you to loop forever. However if you require that one of the arguments always gets structurally smaller each iteration it will be guaranteed to terminate.
This always got me curious - how do you prove that? I mean, it looks like intuitively obvious, do you just bruteforce the state table, showing which states are gonna be switched? I mean, it already looks complicated, we need to see the states of an adder and a comparator for a trivial loop, and if we involve floating point numbers and more complicated logic, it becomes more and more brutal.
And that's not even speaking about hardware bugs. Well, since we try to prove the program, we shall not talk about it, but ultimately it must be done.
>>5035 >Ontology is not physics though, it is philosophy.
This is precisely what epistemology studies. This is a debate of centuries, since Plato > Descartes > Kant > Schoppenhauer up until modern philosophers/logicians (Russel, Wittgenstein, Quine, Putnam, Ian Hacking, etc).
Everything is bonded to reality, because we can't perceive "non-reality". The question is "what is reality" (nature of physics and time, which I think is the same) and how do we communicate this to others (languages/symbols). If you go down this rabit hole, you'll see this is basically a unsolvable problem.
>It's like saying computers do not work since you can not solve the halting problem.
I never said mathematics doesn't work or is useless. Actually I said the opposite in >>5009
>>5039 >oshpark
I've used OSH Park. My problem with them is that they are kind of spendy, slow, and their pcbs have little teeth on the edges where they broke it off from the other pcbs they had fabricated at the same time.
>>5040 Well, that's nice. I've read their quality is not the best, but the prices they offer is really compelling for hobby projects.
What were you working on?
>>5042 >prices are compelling
Yeah, it's probably the cheapest you can get considering there is free shipping. Otherwise getting a low quantity run for cheap means ordering from China and paying for the shipping. If you are planning on ordering from China e-packet will be the cheapest and fastest option. Shipping via e-packet would probably be faster than OSH Park considering the long wait before you get your boards. You'll also likely be able to customize the pcbs you want much more than what OSH Park offers.
>What were you working on
It was a usb <-> serial device. Also was my first time using surface mount components. For your information, I would recommend making sure to get metal stencils and not plastic ones.
It is a secure RISC-V processor, using formal proofs. In the same fashion of previous Crash-SAFE and Draper DOVER. Official page:
https://galois.com/project/besspin/
They will demonstrate the technology this month in the DEFCON 2019 (Las Vegas).
Hensoldt (the company that previously proposed to use RISC-V and seL4 for national security systems) is testing the "Dragonfly" LDM:
>The Lights-Out Digital Manufacturing (LDM) is a manufacturing methodology in which systems run with little to no human intervention, around the clock.
>DragonFly Lights-Out Digital Manufacturing (LDM) printing technology, the industry***s only comprehensive additive manufacturing platform for round-the-clock 3D printing of electronic circuitry.
>The initial deployment took place at the Munich premises of sensor and defense electronics provider HENSOLDT.
https://www.hensoldt.net/press/press-release/news/detail/News/nano-dimension-introduces-dragonfly-ldm-for-continuous-lights-out-digital-manufacturing-of-electron/
Gernot Heiser published a new blog post with some news about seL4:
>[...] Our recent work on time protection indicates that we can solve this problem in seL4, by temporally or spatially partitioning all shared hardware resources, we partition even the kernel. This assumes that the hardware manufacturers get their act together and provide mechanisms for resetting all time-shared resources (and I'm working on the RISC-V Foundation to ensure that RISC-V does)
>[...] And before the end of this year we expect to complete the functional-correctness proofs for the 64-bit RISC-V architecture, as well as the translation-validation toolchain that carries those proofs through to the binary.
>We are also working on verifying the multicore version of seL4. This is challenging because of seL4's uncompromising design for performance, which means that the implementation is racy. Removing races would make the problem far easier to solve, but we won't accept the performance compromises this would imply. After all, our motto is "security is no excuse for poor performance", a core differentiator to other high-assurance systems.
>The MCS model [for realtime scheduling] requires very invasive changes to the kernel, which means re-verifying is a lot of work. However, this work is nearing completion, and we expect MCS to be merged into mainline by the end of this year or early next.
>Our uncompromising performance focus means that we cannot take shortcuts others regularly take, and is, for example, the reason our (high-performance) multicore version is not yet verified. But it'll happen!
>Real-world deployments
>HENSOLDT Cyber is developing a secure hardware-software system, based on their own secure RISC-V chip, and an seL4-based secure operating system. [Disclosure: I'm chief scientist (software) of HENSOLDT Cyber.] It targets critical systems in defence, avionics, industrial automation and automotive.
Hah! I've previously talked about this project here (both in OP and >>5561), but I didn't know Gernot was working as their chief scientist. Nice!
>A USB-based secure communication device, which uses military-strength encryption to communicate via Bluetooth or Wifi,has been evaluated and approved for defence use. To my knowledge this is the first time that software (i.e. seL4) enforced isolation was considered equivalent to air gapping by a certification authority. Itis already in use in several defence forces.
>There are various seL4-based TrustZone TEEs in development. And the Keystone TEE for RISC-V is based on seL4.
Keyboards, pointing devices, power supplies, S/PDIF, Ethernet, and several types of display controllers are old enough that there are plenty of DIY projects and expired patents available.
>>5666 Open Hardware, not "open source". I'm meant the schematics (kicad files). Also, some UPS need firmware such as this 'OpenUPS2':
http://www.mini-box.com/OpenUPS2
I'd start by browsing a Popular Electronics archive. If a project uses ICs that are no longer available or too complex to be trusted, I'd look at their schematics (which are usually available) and recreate it with simpler ICs or an FPGA.
A lot of the simpler stuff, like power supplies, are obvious to anybody who understands electronics. You could design one yourself in an afternoon, or spend the time trawling electronics forums for someone who has already done it and is willing to release his board layout under an open license.
lowRISC blog post explains:
>The RISC-V Compliance test suite is a collaborative effort by the RISC-V Foundation Compliance Task Group to test RISC-V implementations for specification compliance.
The lowRISC core called "Ibex" have added support for automating this process.
https://www.lowrisc.org/blog/2019/08/ibex-code-with-confidence/
The OpenROAD Project from DARPA also added Ibex as a "standard test case". This project was previously mentioned in OP, but here's the actual website:
https://theopenroadproject.org/
It's based on the Western Digital core called "SweRV" and has "a boot ROM, DDR2 controller, on-chip RAM, UART and GPIO". Very nice. It also uses FuseSoC and the RISCV-Complience tests:
https://github.com/olofk/fusesoc
Btw, what a fucking company. Anyway, this is basically the most secure voting system ever made. It's based on RISC-V too and seems to be part of the SSITH program from DARPA. They presented on BlackHat but I couldn't get my hands on this yet. See also (more on that later):
https://securehardware.org/ https://twitter.com/secure_hardware
>>6257 (me)
Continuing. And more from Galois (I would work for free for these guys, just to learn how to be *that* awesome - adopt me Kiniry!).
>MATE is a source-assisted cyber reasoning system for C/C++ that combines whole-program static analysis with established cyber reasoning techniques for low-level vulnerabilities. MATE aims to reason about high-level program design and implementation flaws with the automation and accuracy of existing cyber reasoning systems, detecting complex vulnerabilities that are beyond the reach of existing cyber reasoning systems.
https://galois.com/project/mate/ This is part of the DARPA's CHESS program. They really should add support for Verilog, so people can use this on RISC-V RTLs too. This would be very nice.
Draper Labs also had something similar to it, which I think they used for developing Dover. They call it RIPE (Runtime Intrusion Prevention Evaluator):
https://github.com/draperlaboratory/hope-RIPE
About securehardware.org: They are calling the hardware CASCADES (Configurable, Affordable System-on-Chip for Analysis and Demonstration of Election Security) and are "meant to be finished by April of 2020" and "an E2E-V system will be demonstrated next year on SSITH secure hardware":
https://www.crowdsupply.com/free-and-fair/cascades https://securehardware.org/faq/
This is part of the BESSPIN project, previously mentioned here >>5475 Since Bluespec and lowRISC folks are working together with Galois on it, we can expect something very good out of it. What is not clear for me is the isolation mechanisms. The FAQ notes the CHERI project from SRI/Cambridge, but doesn't explain any further. What about Crash-SAFE and Keystone? And why run FreeRTOS instead of trying to collaborate with Data61/Hensoldt on the seL4 (now that Gernot explained they are getting the realtime kernel formally verified - see >>5656 and also Galois previously worked together on the HACMS project)? And what about the firmware? I've read before Galois worked on the AWS firmware, so we can probably expect a formally verified firmware here. In fact:
>"This demonstration voting system uses a formally verified secure (measured) boot to prove that the (deterministically) compiled voting system software and all of its dependencies (drivers, the RTOS itself, and the state of the devices and their firmware) is exactly what is loaded onto the hardware and initialized."
Since it's a government machine, they could also make the EPROM read-only after flashing the securely-compiled firmware, to make sure reflashing is impossible. To verify, extract the ROM with flashrom and check the hash...
About side-channels:
>"they should still have no means by which to read, leak, side-channel (through digital information flow or timing), or exfiltrate the key."
There's some other potential side-channels, particularly power-analysis, memory attacks (DMA access, cold boots, Rowhammer/RAMbleed, etc), acoustic-cryptoanalysis, TEMPEST, the TRNG/entropy (see >>5039 on the new technique that solves this) and, of course, hardware trojans and implants (which will be the focus of SHIELD program - more on that later).
>"please do not experiment with power glitching attacks***you could fry our expensive FPGA and the device is not built to be resistant to these kinds of attacks, as they are not the focus of this research program or demonstrator"
Well, if you can extract information using this method, then I guess it should be part of the research program.
>deterministically rebuild the system from scratch
There's a potential for compiler attacks here. Are they using CompCert? Have the compiler been bootstraped from scratch? Even though the formal methods will prove the binary itself. The "DeepSpec" research digs into this kind of thing.
>>6258 >I would work for free for these guys
Yeah, I'd like to work their too. I'm in the area, but I'm still going to school. Perhaps I'll apply after I get my masters degree in a couple years.
>>6258 (me)
Ok, so about the SHIELD (Supply Chain Hardware Integrity for Electronics Defense) program from DARPA. Galois will participate too:
>The 100 micrometer x 100 micrometer "dielet" will act as a hardware root of trust, detecting any attempt to access or reverse engineer the dielet.
>The SHIELD dielet design incorporates passive, unpowered sensors capable of capturing attempts to image, de-solder, de-lid or image the IC; mechanical processes that make the dielet fragile and prevent intact removal from its package; a full encryption engine and advanced near-field technology to power and communicate with the dielet.
https://www.darpa.mil/program/supply-chain-hardware-integrity-for-electronics-defense
Some issues can be risen here that can be very complicated to solve.
The first is how you detect hardware implants, as mentioned here >>4973 and here >>5019 . These might be solvable through optical analysis (since they are big enough), but this might not cover 100% of the possibilities and is probably not efficient enough for large scale foundries (in the level of TSMC/GlobalFoundries).
So the issue for SHIELD becomes how to make sure that the RTL sended to the foundry is *exactly* what is described, nothing more and nothing less. This can be nearly impossible. The signoff process cannot be perfect against attacks like A2:
https://en.wikipedia.org/wiki/Signoff_(electronic_design_automation)
https://en.wikipedia.org/wiki/Physical_verification
And there's also the issue of photomasks. It's a very complex and delicate process and has high costs. There's only a few companies that are making these and they have too much power in their hands:
https://en.wikipedia.org/wiki/Mask_inspection
A hypothetical attack I can see is on the electron-beam. They probably run a firmware on these machines and if you can replace this firmware it might be possible to implant backdoors like A2 into many different ICs (including SHIELD).
This is a serious issue that I think DARPA and NSA should be looking, because attacks of this level can affect national security.
The only way I can see for SHIELD to succeed is reducing the attack surface making a model for a "lights-out" or "No Humans in the Loop" foundry, the same way Hensoldt seems to be doing (see >>5561 ), where everything is hermetic locked, employers put the silicon on one side, load the verified RTL+SHIELD and... poof, the IC appears on the other end like magic. Of course, this is not realistic.
>The SVF block disables TV trace transmission if there is no active PCIe link
So it only works if it has DMA link? Doesn't this open to other possible attacks (such as pcileech)?
https://github.com/ufrisk/pcileech/
>A future version of the SVF will provide a register for programmatically enabling and disabling TV trace generation
The "TV" feature should be mandatory and impossible to disable. I hope they meant this just for prototypes.
And the last comment for today (or this week): I've mentioned the manycores OpenPiton/Ariane and BaseJump before on >>4911 , but there is two more projects in the field of high-performance RISC-V.
The first is OpTiMSoC:
>"OpTiMSoC stands for Open Tiled Manycore System-on-Chip. It is an open-source framework primarily written in Verilog which allows you to build your own manycore System-on-Chip by connecting tiles like processors and memories through a Network-on-Chip. The resulting system can then be simulated on a PC or synthesized for an FPGA."
https://www.optimsoc.org/index.html
And GoblinCore64:
>"The GoblinCore64 (herein referred to as GC64) that was originally designed to facilitate the construction of a high performance core architecture that was well-suited to executing applications traditionally known as 'data intensive.' These applications generally refer to algorithms that operate on sparse data structures such as graphs, sparse matrices and/or perform nonlinear combinatorial operations (et.al.)."
http://gc64.org/?page_id=21
RISC-V is just too good to not be successful. I'll make a prediction here: in the beginning of 2030's, RISC-V will be in the TOP500 list.
>>6262 Just a correction: OpTiMSoC is not based on RISC-V. But it's a open source framework, so it might be possible to make a 'cross-pollination' between other cores such as Ariane.
They now seem to be collaborating. According to Luke, there's 50+ people on their team and now more people from Simple-V, all looking to solve the lack of GPU in the RISC-V world.
This is going faster than I thought!
Another news:
>be trusted
>Today's enclaves protect only certain cryptographic secrets, such as private keys. These enclaves lack human-friendly I/O and must delegate the task of rendering and recording information to a less secure host.
>Betrusted solves this problem by incorporating easily auditable Human-Computer Interaction (HCI) elements to the security enclave. Betrusted ensures that human-readable secrets are never stored, displayed, or transmitted beyond the confines of the betrusted device: betrusted is a security enclave with human-friendly I/O.
This is a project from Andrew Bunnie (same creator of Novena laptop and USB ROM exploits) and is based on RISC-V:
https://betrusted.io/
>>6689 Most of the development now is on the embedded systems (in special Zephyr and FreeRTOS). The idea is that RISC-V should first be adopted in the microcontroller world, to then advance into complex SoCs.
But the debian port is not dead, just slow. We will see growing development in the following 5 years or so in the linux kernel. NetBSD also is doing a initial port to RISC-V, btw.
>>6262 (me)
>This is not supported by open source tools like SymbiFlow and PRGA.
In the presentation from Kiniry (>>6732), he explains:
"Because the CPU we are developing run on high-end Xilinx FPGA's, which are very costly, we wanna democritize red teaming and develop a variant that will run on low-cost FPGA's that run with open source design tools".
Gernot Heiser will discuss Timing-Attacks on the conference "SHARD":
>[...] we must complement memory protection by time protection. However, I will demonstrate that the present hardware-software contract, the ISA, by being a purely operational contract abstracts too much of the hardware to allow the OS to provide time protection.
>This situation can only be remedied by extending the contract to give the OS the right tools for enforcing security. I will discuss the proterties the new contract must define, and how we can hope to use it to achieve provable time protection.
This conference also will have other talks related to side-channels in hardware (mostly with a RISC-V focus).
The conference OSFC_IO also happened this last week, with lots of firmware related talks. Unfortunatelly nothing about RISC-V, AFAIK.
On the ERI Summit 2019, DARPA released other talks than >>6732 about secure hardware and efficient hardware design. I couldn't watch everything yet, but when I do I'll shared some notes...
Another one was SpISA this last week. Two talks from Galois (related to reverse engineering and formal RISC-V verification) and one from Sail (pic related).
>>6689 Just one week after your comment and this happens:
>Linux 5.3 Released After Extra RC, Brings Numerous RISC-V Improvements
>These include image-header support for RISC-V kernel binaries, designed to be compatible with ARM64 image headers, a two-stage initial page table setup process, support for CONFIG_SOC starting with SiFive's range of RISC-V systems-on-chips, DT data for the SiFive FU540 and HiFive Unleashed's gigabit Ethernet controller, support for PCI Express message-signalled interrupts, and support for the new clone3 RV64 syscall.
https://abopen.com/news/linux-5-3-released-after-extra-rc-brings-numerous-risc-v-improvements/
OneSpin released a article on the eeNewsEurope magazine, talking about formal verification of highly complex SoC.
This is very important, because SoC verification is very complicated, as they explain:
>At the recent Design and Verification conference (DVCon) in China, Xilinx and OneSpin presented a case study of the OneSpin Connectivity XL App applied to a multi-billion-gate SoC.
>Using 7 nm technology, this chip contained 60 million instances of 35 thousand modules, 90 million flip-flops, and 80 thousand finite state machines.
>Connectivity XL found several corner-case bugs that would have been very hard to detect using any other tool or method. The errors included incorrect block integration, multiple drivers enabled on paths, and re-convergent paths. The debug information provided enabled easy root-causing, even on paths with more then two thousand signals between source and destination.
>There were no inconclusive results for any connections
From ABOpen:
>"One of the main motivations leading to the design of an open source DMA controller was the lack of portable open source alternatives to proprietary controllers provided by FPGA vendors"
>"The integration of FastVDMA with a portable SoC, such as LiteX, would solve the portability and platform-dependence of any DMA-based designs, and so allow for more engineering freedom in our FPGA projects"
https://abopen.com/news/antmicro-releases-fastvdma-open-source-resource-light-dma-controller/
This will make easier to port systems compiled with Clang (FreeBSD/OpenBSD). Also, as Alex Bradbury said, programming languages like Rust/Julia and Swift. Congrats lowRISC team!
>The core of the design is to produce a secure electronic voting machine, a goal which, in our opinion, is likely unachievable
Not true. This is the Nirvana fallacy right here. "Secure" doesn't mean "perfectly secure".
>based on a 64-bit RISC-V core running FreeBSD
I think this is the CHERI one. The Galois prototype is running FreeRTOS, AFAIK.
Neither of those are secure, by the way. They should be using seL4.
>RISC-V-based general-purpose graphics processing unit (GPGPU)
I think this is the OpenCelery project. ABOpen should've specificed that.
>IBM releases Open Memory Interface
Here's the code:
https://github.com/OpenCAPI/omi_device_ice https://github.com/OpenCAPI/omi_host_fire
>LoRaWAN
This is nice, but they keep pushing it as if it was open and it's not. Some groups should put pressure on them to release it as a open standard, just like DASH7 did. I find this very importat from a security stand-point (see BLEEDINGBIT vulnerability).
The guys from ABOpen need some Galois-approved coffee.
It adds a memory protection mechanism as a extension. For details see the github. Don't know how that compares with Galois CASCADES, Crash-SAFE or Ibex. But I guess it's a 'primitive' project compared to these others. Still, nice job.
Another news: related to hardware verification as pointed in >>6260, a new research came about. The technique is called "ptychographic X-ray laminography" and it's able to accurately analyse IC's in a non-destructive way (you can still use it afterwards). This is very relevant to reveal possible hardware implants (like A2 hardware) or deliberate modification of the reference RTL:
https://www.nature.com/articles/s41928-019-0309-z https://zenodo.org/record/2657340
>>5019 Related to implants and BadUSB, see these too:
>Deploy WHID on Victim's machine and remotely control it by accessing its WiFi AP SSID.
https://github.com/whid-injector/WHID >P4wnP1 A.L.O.A. by MaMe82 is a framework which turns a Rapsberry Pi Zero W into a flexible, low-cost platform for pentesting, red teaming and physical engagements
https://github.com/mame82/P4wnP1_aloa >TURNIPSCHOOL is a hardware implant concealed in a USB cable. It provides short range RF communication capability to software running on the host computer. Alternatively it could serve as a custom USB device under radio control.
http://www.nsaplayset.org/turnipschool
We had a thread about acoustic side-channel other day. I can post here some information I have about all kinds of side-channel attacks. It's kinda off topic, so I'll only do that if someone is interested...
>>7985 >and it's able to accurately analyse IC's in a non-destructive way
That sounds useful. Especially if there are rare chips, it would be a shame to have to have to destroy the chip to take layer by layer images of the chip.
Aparently the NSCU (North Carolina State University) developed a open source PDK called FreePDK. It does LVS (Layout versus Schematic) verification, as mentioned here >>6260 . This is essential for making ASICs and no one except NCSU seems to be paying attention to it. Props for them. I wonder if DARPA wouldn't be interested in a merge of OpenROAD and FreePDK...
Pic related. Couldn't find the recording of Luis Rueda's talk. Might be posted soon on fossifoundation channel.
But, from the tweet, they seem to have developed a "in-house std-cell generator" instead of using Silvaco tools.
I'm really looking forward to watch this video. I think the processes from RTL to 'tape-out' is one of the big essential points not just for RISC-V to succeed in the future, but also to have better security assurances.
>>7991 Is the blue shaded sections the parts which do not have a free software alternative, or do the "No OS", still need it too? I do not quite understand what it means by "No OS."
>oreboot is a downstream fork of coreboot, i.e. oreboot is coreboot without 'c'.
>oreboot will only target truly open systems requiring no binary blobs. For now, that means no x86.
>oreboot currently only plans to support LinuxBoot payloads.
From the commits, only two guys seems to be working on it: one from google, other from western digital. Two supporters of RISC-V Foundation. The first board to add 'support' was HiFive Unleashed.
Very exciting! Just wish they used Haskell instead of Rust... this would make it easier to get the code formally verified in the future.
>>7998 I'm another lurker of this thread since a long time, i'm really interested in RISC-V and its future, but to be honest i lack the knowledge to contribute to this thread and the time to properly follow all the development. Your posts are much appreciated.
More news.
LibreSilicon:
>"We develop a free (as in freedom, not as in free of charge) and open source semiconductor manufacturing process standard, including a full mixed signal PDK, and provide a quick, easy and inexpensive way for manufacturing. No NDAs will be required anywhere to get started, making it possible to build the designs in your basement if you wish so. We are aiming to revolutionize the market by breaking through the monopoly of proprietary closed source manufacturers!"
https://libresilicon.com/
This seems fucking great. One of the companies participaing is "efabless" (printed the Raven processor, in OP pic). I think the people behind it is the same maintaining Librecores.org (not sure, though).
But Luke (main developer of this project) is doubtful about patents:
>"to even *try* to avoid these [patents] is just completely pointless: the entire design would be so hamstrung as to be utterly commercially useless, and, worse than that, we'd be taking on far more work and would completely miss the goal as a result, missing out on additional funding opportunities that would enable us to actually get to first silicon."
He also is not happy with the RISC-V Foundation:
>"There is huge momentum around RISCV itself, however as far as open *innovation* is concerned, the sheer arrogance of the Foundation in failing to respect the combination of Libre goals and business objectives has us completely isolated from key critical resources such as the closed secret lists and wiki."
http://lists.libre-riscv.org/pipermail/libre-riscv-dev/2019-October/003035.html
If you ask me, I'd say he was a fool in this last comment. Doing that will just fragment a community that is slowly having industry adoption. These kind of comments are one of the reasons people don't like "free software" (read: GNU/FSF-supporters).
RISC-V Foundation is certainly not perfect, and everyone has the right to complain, but a better way to solve it is to get in contact with them privately.
Samsung might use RISC-V in their next Exynos processor. This is not confirmed yet, but if true this will be *huge* for RISC-V. The report comes from Korea, translated here:
>"Now, we've learned that Samsung will fabricate a SoC using SiFive IP on the 14nm Low Power Plus node."
https://wccftech.com/samsung-risc-v-chip-14nm/
ps: video unrelated to this news, but related to the thread.
>>8024 >>8145 Nice. It's good to see other people here.
>Your posts are much appreciated.
You're welcome. Hope it's not getting too difficult to follow. Sometimes there's just too many projects popping up and it's difficult to remember which is which.
I have just applied to Galois for an internship this summer. Considering I have experience in both functional programming and embedded development hopefully I am a good match to what they are looking for. I hope I get to work on some cool RISC-V stuff or other formal verification tools. Wish me luck.
>>8349 Hoah! Good luck anon. You're doing what I would call the closest thing for me of a "dream". I wish I could do that too and I hope you succeed.
Galois is such an amazing company. I'm trully a fanboy, no shame.
Hope you get some work on the CASCADES project. Also, it would be a bonus for you if you get into Bluespec language. It has the same syntax from haskell, so I think you'll be good at it (Galois is using it a lot):
https://github.com/rsnikhil/Bluespec_BSV_Tutorial
I was not able to watch it yet. When I do I'll put my notes here.
Another news: SiFive released "Shield" and "WorldGuard". It's supposed to offer "per-memory protected memory regions and multi-core privilege modes" to RISC-V. This seems to be a tagging system: give a ID to each process and isolate them according to each area. They mention those areas: cache, interconnect, peripherals, bus masters, DMA regions, and memories. Seems interesting, specially for DMA as they mention, because GPU's today (or any PCIe device really) have basically unrestricted access to memory and this is a major security threat in my opinion.
The SiFive Shield is meant to be a "root of trust" (another buzzword industry is trying to push). Basically it creates cryptographic sign and keys for each device. This would enable to have trusted boot and firmware, apparently. The issue I see here is that they have a "NIST SP 800-90A/B/C compliant true random number generator (TRNG)" inside it, and that cannot be verified after they are printed on silicon. Sure we can see the RTL as it is open (is it? couldn't find the source), but can we trust all our cryptography to this TRNG? What if someone makes it generate deterministic numbers? Dunno.
They have SHA-3 (Blake2) support though, which I find cool.
Blog post is here:
https://www.sifive.com/blog/sifive-shield-an-open-scalable-platform-architecture
This is a collaboration with lowRISC team (and it seems Western Digital also worked on it). The idea is basically the same, to secure the firmware and boot stages. Unlike SiFive's, it has easily accessible RTL sources, specifications and seems to be well documented.
My overall opinion: I feel more positive about OpenTitan than SiFive. Let's not forget Google research teams also contributed to Coreboot in the past, so this might open some doors to Coreboot (or oreboot, see >>8017) on RISC-V.
SiFive's idea about "multi-level" security seem flawed. This will increase complexity and make it too difficult to use formal methods. Simpler solutions such as the CASCADES tagging from Galois and capability-based isolation should be a better fit to solve the problem.
Also, I don't know how those mechanisms compare to other solutions like Keystone. I think that, in an ideal world, we would see alliances between those companies, so they stop competing and get a true and well-designed standard. But we're not in an ideal world anyway. Hope CHIPS Alliance and OpenHardware Group come together to create more consensus on the matter.
Last news: Hensoldt released a video on twitter, where they mention the "National Secure Mode Cryptographic Computer". This might be the project Gernot Heiser is working to unite RISC-V and seL4. This system is meant to protect Air Defense of France. Since this is the military, there's no information online about this and I'm just supposing this is the case. The video was uploaded in this reply.
>>9161 >OSHPark
The best part thing about OSHPark is there shipping prices. The worst part is the delay it takes to get your PCB's manufactured. If you would likely them quickly your best option is to get them epacketed over from China.
And this is why we need coreboot on RISC-V:
>Researchers at ForAllSecure found the flaws in U-Boot's file system drivers. They include a recursive stack overflow in the DOS partition parser, a pair of buffer-overflows in ext4 and a double-free memory corruption flaw in ext4. They open the door to denial-of-service attacks, device takeover and code-execution.[...] ForAllSecure also found five low-severity divide-by-zero bugs, triggered by invalid extended file systems.
https://firmwaresecurity.com/2019/11/08/cve-2019-13103-u-boot-amazon-kindle-embedded-devices-open-to-code-execution/
>>9340 Is someone finally going to put a hardware switch on one, so the firmware can only be "updated" when manually toggled? Or a similar switch to put it enable RO mode?
The idea is that you compile your firmware, flash it and then solder the EPROM pins. This will make it impossible to reflash it again without resoldering those pins.
This might not be a good idea, though, since Coreboot is not perfect and will have vulnerabilities at some point.
A better idea might be to just lock the laptop in some box, like those rugged cases sold by Pelican. Put a good lock on it and done. This will protect not just against firmware reflashing attacks, but also hardware implants.
hifive1-protector:
>Hifive1 + Hifive1-revB "bootloader" code to protect against bricking written in Rust.
>is meant to prevent getting the hifive1 and hifive1-revB boards into an un-flashable state.
https://github.com/almindor/hifive1-protector
There's a small community trying to use Rust for RISC-V development. The rboot could be used together with oreboot (see >>8017 - btw, they are planning to support lowRISC Ibex, it seems).
Found more neat projects. TinyUSB:
>TinyUSB is an open-source cross-platform USB Host/Device stack for embedded system, designed to be memory-safe with no dynamic allocation and thread-safe with all interrupt events are deferred then handled in the non-ISR task function.
https://github.com/hathach/tinyusb
And ValentyUSB (supposedly based on TinyUSB):
>USB Full-Speed core written in Migen/LiteX. This core has been tested and is known to work on various incarnations of Fomu. It requires you to have a 48 MHz clock and a 12 MHz clock. It optionally comes with a debug bridge for debugging Wishbone.
https://github.com/im-tomu/valentyusb
I think this is a good move. LowRISC is also in close colaboration with ETH Zurich, so this might facilitate communication. China many chinese companies have interest in RISC-V (Alibaba and Baidu, for example), and it wouldn't be good if the foundation loses them.
Another news is a research about a RISC-V based processor with resistance to power analysis side-channel, called PARAM:
https://arxiv.org/abs/1911.08813
Btw, Bluespec was responsible by the Draper DOVER processor, which uses micropolicies and also the basis for Galois processor used in the SSITH Darpa program.
The idea is basically of two systems running at the same time and one check the another. This increases resiliency to memory corruptions, common in satellites. This might also be useful for other applications, such as lower risks of failure (necessary for some high assurance systems). Pic related.
Last update is about MNT Reform. Not RISC-V related, but the project is interesting and might be useful when someone releases a high powered risc-v SoC. They seem to be doing well and almost ready to ship. Updates on their Mastodon:
https://mastodon.social/@mntmn
Hence why firmware security is important. RISC-V boards shouldn't just adopt u-boot by default. CHIPS Allience and OpenHW Group should push more for coreboot or oreboot once the SoCs start to kick off. We'll see.
>>9773 >PARAM
I wonder if it's possible to modify the scheme so it only obfuscates memory based off a tag bit. Maybe it would help the performance. I'm not positive it would though. It might just be a constant hit no matter what since the max clock rate that part of the circuit supports limits the whole thing.
Also, it's been over a month and still no word back from Galois. Next time they host a talk I'm going to try and attend and do some networking.
>>9783 >only obfuscates memory based off a tag bit
Good point. But I think it would still be succeptible to leaking information, particularly cryptography secret keys ("branch predition units"). To be specific, in page 2 they say their framework protects "register bank, cache memory, control status registers, execute stage units and pipeline buffers".
So, if their method was applied only to tagged memory, all of these would still leak, except for cache memory and perhaps pipeline buffers.
Also, the overhead is quite small. Page 9 says "the maximum clock frequency reduced from 48MHz in Shakti-C to 33MHz in PARAM" and "the cycles per instruction (CPI) for the processor is the same as that of Shakti-C".
>>9786 >Also, the overhead is quite small. Page 9 says "the maximum clock frequency reduced from 48MHz in Shakti-C to 33MHz in PARAM"
They are losing about a third of the performance. At least to me that seems more than a small performance hit. Speed might not be a huge problem though. Perhaps you can delegate a chip like this to be some sort of security coprocessor.
>Did you use the informations from this page?
Yeah, I applied through their official means.
>If yes, maybe try to contact someone more personally, such as Dan Zimmerman
That would probably be a good idea to do, but due to their kind of fluid role system I can not easily find out who are a part of Galois' hiring process. Perhaps just asking anyone their could get me forwarded to the right person though.
>>9787 >seems more than a small performance hit.
You might be right. Don't know if this performance hit would grow exponentially as processor frequency increases too or if this is a constant.
Still, I think it's great that more research is comming in the side-channel hardware protections. Gernot also published his considerations about timing side-channels on hardware some months ago, so this is a growing field.
Speaking of coprocessor, found this company:
https://hex-five.com/ Doesn't seem to be open sourced, though. Based on RISC-V and member of the foundation.
These people should stop fighting and unite to build a future standard. Now we have about 4 secure coprocessors (Keystone, OpenTitan, HexFive and SiFive Shield), all of which work differently but have the same purpose. If they got together they could get the best practices and build something much stronger.
>I can not easily find out who are a part of Galois' hiring process
Try twitter. Seriously. Many people from Galois is very active and open on twitter, including @kiniry and past employers. You can find them because they retweet from @galois, @free_and_fair or @secure_hardware
>>9788 >Don't know if this performance hit would grow exponentially as processor frequency increases too or if this is a constant
I do not think it is a constant hit, but I do think the amount you have to slow down the clock to add this in decreases as your frequency increases.
>Try twitter. Seriously.
I think I'll just try my luck through email as I do not have, nor wish to create a twitter account for this.
The gaps are closing for RISC-V. This is something I never thought would be possible. We might actually be able to buy fast RISC-V SoC in the next 10 years (fast == comparable speed with more modern ARM processors, such as i.MX6).
>Formal specification is now frozen https://riscv.org/specifications/
https://github.com/rsnikhil/Temporary_TGISA
>More than 60 designs open sourced already and more every day:
https://github.com/riscv/riscv-cores-list
>Not even including secure enclaves and GPU:
https://keystone-enclave.org/
https://libre-riscv.org/simple_v_extension/
>Open software for FPGA designs with Yosys, Symbiflow, Nextpnr and nMigen https://symbiflow.github.io/
>Open hardware for FPGA such as TinyFPGA, Rodiona ULX3S, BlackIce and Fomu
https://twitter.com/ico_TC
https://github.com/emard/ulx3s
>Efforts to use formal methods and increase hardware security by many companies: DARPA's CRASH-SAFE, Draper Labs (DOVER), OneSpin, Bluespec, Axiomise, BAE Systems, etc.
>People developing formally verified software for it: Galois, Data61, Hensoldt, Critical Systems, ADA Company
>Firmware already open source, but Coreboot being ported:
https://doc.coreboot.org/mainboard/sifive/hifive-unleashed.html
>Industry partnership with many high-level companies, including Western Digital, Nvidia, Google, Microsoft, between others.
>Industry groups such as OpenHWGroup:
http://openhwgroup.org/
>Support software such as OpenROAD:
https://github.com/The-OpenROAD-Project/alpha-release
>Companies more open to print your custom IP:
https://efabless.com/faq
>Open PCB design software:
http://www.kicad-pcb.org/
>Debian and Clang added support for RISC-V
>Nice community growing educational material every day
FUCK YEAH!