"Blackphone" said to be "a super-secure nsa-proof"
http://www.yahoo.com/tech/startup-launching-a-super-secure-nsa-proof-7351109... Fears over NSA spying have prompted people around the world to think about security differently, whether it be petitioning for companies to better secure their data or changing the information they share online. In particular, security around smartphones has been of great concern, as people increasingly surf the Web, make calls and send messages from their mobile devices. An international group of privacy enthusiasts has come together to create Blackphone, a smartphone that claims it will help to better protect your information. Mashable writes that Blackphone is the brainchild of Silent Circle and Geekosphere, with participation from big players in the fight for information privacy and computer security. Phil Zimmermann, creator of data encryption protocol PGP (Pretty Good Privacy), is one of the minds behind the device. “Blackphone provides users with everything they need to ensure privacy and control of their communications, along with all the other high-end smartphone features they have come to expect,” Zimmerman said, according to Mashable. [ Right Click: Kiwi lifestyle tracker to free people from their smartphones ] The operating system is a custom build of Android OS called PrivatOS, designed for improved security. Silent Circle’s CEO Mike Janke says the project will be open source, as will the PrivatOS operating system. The phone likely won’t have the most outstanding specs, but the team says that’s because privacy is the top concern. No specific details have been given about the phone yet (although some of the code has been posted to GitHub). The companies say they’ll be unveiling it properly at Mobile World Congress in Barcelona beginning Feb. 24. Even with very little information about the device currently available, some media outlets are suggesting that the phone could be “NSA-proof.” That’s a tall order, especially in light of a story from The New York Times claiming that the NSA has implanted software in nearly 100,000 computers to create backdoor radio access. For more information on Blackphone, visit its website at https://www.blackphone.ch.
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 The only almost-safe portable phone I can imagine is a purely VoIP phone, and that comes with a ton of caveats and precautions. It's a very difficult problem. That whole corporate-locked-in-baseband thing seems to throw a curveball at any ideas I can think of when trying to execute a secure cellular device. I am, however, excited to see Zimmermann involved. Sam On Fri 17 Jan 2014 01:25:50 AM PST, Jim Bell wrote:
http://www.yahoo.com/tech/startup-launching-a-super-secure-nsa-proof-7351109...
Fears over NSA spying have prompted people around the world to think about security differently, whether it be petitioning for companies to better secure their data or changing the information they share online. In particular, security around smartphones has been of great concern, as people increasingly surf the Web, make calls and send messages from their mobile devices. An international group of privacy enthusiasts has come together to create Blackphone, a smartphone that claims it will help to better protect your information. Mashable writes that Blackphone is the brainchild of Silent Circle and Geekosphere, with participation from big players in the fight for information privacy and computer security. Phil Zimmermann, creator of data encryption protocol PGP (Pretty Good Privacy), is one of the minds behind the device. “Blackphone provides users with everything they need to ensure privacy and control of their communications, along with all the other high-end smartphone features they have come to expect,” Zimmerman said, according to Mashable. [ Right Click: Kiwi lifestyle tracker to free people from their smartphones ] The operating system is a custom build of Android OS called PrivatOS, designed for improved security. Silent Circle’s CEO Mike Janke says the project will be open source, as will the PrivatOS operating system. The phone likely won’t have the most outstanding specs, but the team says that’s because privacy is the top concern. No specific details have been given about the phone yet (although some of the code has been posted to GitHub). The companies say they’ll be unveiling it properly at Mobile World Congress in Barcelona beginning Feb. 24. Even with very little information about the device currently available, some media outlets are suggesting that the phone could be “NSA-proof.” That’s a tall order, especially in light of a story from The New York Times claiming that the NSA has implanted software in nearly 100,000 computers to create backdoor radio access. For more information on Blackphone, visit its website at https://www.blackphone.ch.
- -- http://about.me/sam.gordon Keep the net free Electronic Frontier Foundation https://supporters.eff.org/donate Free Software Foundation https://my.fsf.org/associate/support_freedom/join_fsf -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.14 (GNU/Linux) Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/ iQEcBAEBAgAGBQJS2PrJAAoJEBNrXBfj4zc+lqAIAIpTi9wtUfXGIZSgZGk0LcCn jVTjpg6ZSd6C8uIrYPmXFiiy0DCnb1aj4ca6BoFRVbrVVad64ED4e/zqkM4lAqTU 9IilvLfzeTcX04OmZsXgU+644ymjODO5l/wb/hL1/DdQTHnyz91IzKZsocI7d3Cw Aatm0vEquUmwR0eT10LWto2F+phQze0OpMGLxCa/KN5+/q+Yk5MQ9o/wuEj2ePhu cUJOv8lFjkl+rbSC+6X1rIhaa89mKjlz8tLlXQYUj/++c5vXhDyMIe0lQratgzMm o076UvIhCeo7yz4ct5NzKFISSGW7CrTHt1xjQF1ybM6Nt1FV/wKxpTwBRB8qc1A= =dGK5 -----END PGP SIGNATURE-----
They should be able to do blackphone to blackphone secure voice and text reasonable well. Other android apps and phone location tracking, not so much. -Lance -- Lance Cottrell loki@obscura.com On Jan 17, 2014, at 1:41 AM, Sam Gordon <segordon@gmx.com> wrote:
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
The only almost-safe portable phone I can imagine is a purely VoIP phone, and that comes with a ton of caveats and precautions. It's a very difficult problem.
That whole corporate-locked-in-baseband thing seems to throw a curveball at any ideas I can think of when trying to execute a secure cellular device.
I am, however, excited to see Zimmermann involved.
Sam
On Fri 17 Jan 2014 01:25:50 AM PST, Jim Bell wrote:
http://www.yahoo.com/tech/startup-launching-a-super-secure-nsa-proof-7351109...
Fears over NSA spying have prompted people around the world to think about security differently, whether it be petitioning for companies to better secure their data or changing the information they share online. In particular, security around smartphones has been of great concern, as people increasingly surf the Web, make calls and send messages from their mobile devices. An international group of privacy enthusiasts has come together to create Blackphone, a smartphone that claims it will help to better protect your information. Mashable writes that Blackphone is the brainchild of Silent Circle and Geekosphere, with participation from big players in the fight for information privacy and computer security. Phil Zimmermann, creator of data encryption protocol PGP (Pretty Good Privacy), is one of the minds behind the device. “Blackphone provides users with everything they need to ensure privacy and control of their communications, along with all the other high-end smartphone features they have come to expect,” Zimmerman said, according to Mashable. [ Right Click: Kiwi lifestyle tracker to free people from their smartphones ] The operating system is a custom build of Android OS called PrivatOS, designed for improved security. Silent Circle’s CEO Mike Janke says the project will be open source, as will the PrivatOS operating system. The phone likely won’t have the most outstanding specs, but the team says that’s because privacy is the top concern. No specific details have been given about the phone yet (although some of the code has been posted to GitHub). The companies say they’ll be unveiling it properly at Mobile World Congress in Barcelona beginning Feb. 24. Even with very little information about the device currently available, some media outlets are suggesting that the phone could be “NSA-proof.” That’s a tall order, especially in light of a story from The New York Times claiming that the NSA has implanted software in nearly 100,000 computers to create backdoor radio access. For more information on Blackphone, visit its website at https://www.blackphone.ch.
- -- http://about.me/sam.gordon
Keep the net free
Electronic Frontier Foundation https://supporters.eff.org/donate
Free Software Foundation https://my.fsf.org/associate/support_freedom/join_fsf -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.14 (GNU/Linux) Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/
iQEcBAEBAgAGBQJS2PrJAAoJEBNrXBfj4zc+lqAIAIpTi9wtUfXGIZSgZGk0LcCn jVTjpg6ZSd6C8uIrYPmXFiiy0DCnb1aj4ca6BoFRVbrVVad64ED4e/zqkM4lAqTU 9IilvLfzeTcX04OmZsXgU+644ymjODO5l/wb/hL1/DdQTHnyz91IzKZsocI7d3Cw Aatm0vEquUmwR0eT10LWto2F+phQze0OpMGLxCa/KN5+/q+Yk5MQ9o/wuEj2ePhu cUJOv8lFjkl+rbSC+6X1rIhaa89mKjlz8tLlXQYUj/++c5vXhDyMIe0lQratgzMm o076UvIhCeo7yz4ct5NzKFISSGW7CrTHt1xjQF1ybM6Nt1FV/wKxpTwBRB8qc1A= =dGK5 -----END PGP SIGNATURE-----
Hi All, Unfortunately there are NO guarantees of NSA proof claims, Phil above all knows this after having designed version after version of insecurity with pgp, bassomatic and web of evidence being only 2 examples that went public,(dont even get me started on the DSA key mess...) Similar bumps in the road were noted during ZRTP development.. Now in the secure phone case .. there is NO way to know that you are secure against NSA TAO even if ALL source code to the phone apps and the base band processor firmware is published.. not even if the VHDL code for the IC design is published.. does mean we stop trying and give up?? hell no...think of it as a economic problem even classifying enough crypto at realtime speeds for capture turns into a major pain the the ass even on Narus boxen. And enough PFS-type systems ie DH ephemeral key exchange systems deployed and the headache grows even more... but all claims of NSA proof are indeed basically somewhat fraudulent as its a guarantee that no one checked out the chip design software for auto insert logic additions to their cell libraries. And with TAO placing teams of engineers its almost a sure bet that the IC libs are contaminated either with active flaws or simply important ones that never got reported. And etc ad nauseam from the silicon on out.. we should just stop using loaded language like "NSA Proof" and resting on past laurels to assure folks that such is a fact(it isn't). gh(who is now finally picking up the python language in a serious way) ps "Violent Python"(the book) rocks! next will be taking pbp routines and formats and creating a new curvep25519 version of type 1 and type 2 remailers with a nym.alias.net clone in python using Curvep25519 keys to emulate a type 1 reply block(have to see what mixminion does for reply-blocks if any) ps2ps: PCP and PBP developers need to make up their collective heads about external representation key formats for public keys(I will be using pbp as its already in python) I am kind of dependent on these(key format representations) On 1/17/14 1:25 AM, Jim Bell wrote:
http://www.yahoo.com/tech/startup-launching-a-super-secure-nsa-proof-7351109...
Fears over NSA spying have prompted people around the world to think about security differently, whether it be petitioning for companies to better secure their data or changing the information they share online. In particular, security around smartphones has been of great concern, as people increasingly surf the Web, make calls and send messages from their mobile devices. An international group of privacy enthusiasts has come together to create Blackphone, a smartphone that claims it will help to better protect your information. Mashable writes that Blackphone is the brainchild of Silent Circle and Geekosphere, with participation from big players in the fight for information privacy and computer security. Phil Zimmermann, creator of data encryption protocol PGP (Pretty Good Privacy), is one of the minds behind the device. “Blackphone provides users with everything they need to ensure privacy and control of their communications, along with all the other high-end smartphone features they have come to expect,” Zimmerman said, according to Mashable. [ Right Click: Kiwi lifestyle tracker to free people from their smartphones ] The operating system is a custom build of Android OS called PrivatOS, designed for improved security. Silent Circle’s CEO Mike Janke says the project will be open source, as will the PrivatOS operating system. The phone likely won’t have the most outstanding specs, but the team says that’s because privacy is the top concern. No specific details have been given about the phone yet (although some of the code has been posted to GitHub). The companies say they’ll be unveiling it properly at Mobile World Congress in Barcelona beginning Feb. 24. Even with very little information about the device currently available, some media outlets are suggesting that the phone could be “NSA-proof.” That’s a tall order, especially in light of a story from The New York Times claiming that the NSA has implanted software in nearly 100,000 computers to create backdoor radio access. For more information on Blackphone, visit its website at https://www.blackphone.ch.
-- Tentacle #99 ecc public key curve p25519(pcp 0.15) 1l0$WoM5C8z=yeZG7?$]f^Uu8.g>4rf#t^6mfW9(rr910 Governments are instituted among men, deriving their just powers from the consent of the governed, that whenever any form of government becomes destructive of these ends, it is the right of the people to alter or abolish it, and to institute new government, laying its foundation on such principles, and organizing its powers in such form, as to them shall seem most likely to effect their safety and happiness.’ https://github.com/TLINDEN/pcp.git to get pcp(curve25519 cli) https://github.com/stef/pbp.git (curve 25519 python based cli)
On Sat, Jan 18, 2014 at 12:16 PM, gwen hastings <gwen@cypherpunks.to> wrote:
... Now in the secure phone case .. there is NO way to know that you are secure against NSA TAO even if ALL source code to the phone apps and the base band processor firmware is published.. not even if the VHDL code for the IC design is published..
does mean we stop trying and give up?? hell no...think of it as a economic problem even classifying enough crypto at realtime speeds for capture turns into a major pain the the ass even on Narus boxen.
indeed, useful as a cost deterrent even if fallible. and of course, it's fun trying to protect against these attacks (e.g. playing on "Hard Mode"). for some definition of "fun"...
but all claims of NSA proof are indeed basically somewhat fraudulent as its a guarantee that no one checked out the chip design software for auto insert logic additions to their cell libraries. And with TAO placing teams of engineers its almost a sure bet that the IC libs are contaminated either with active flaws or simply important ones that never got reported. And etc ad nauseam from the silicon on out..
the short list of mandatory steps to play the game: - never mess up! one mistake can be catastrophic. (this means developing habits) - source all hardware through retail outlets paid in cash. (avoid targeted supply chain inserts) - review all open source components related to key generation, management, derivation, zeroisation. or have someone you trust do so. (see also: crowd funded TrueCrypt audit) replace unsatisfactory parts with better ones. (still using my own rngd; so glad to not have to roll my own FDE boot and key mgmt anymore!) - use extensive defense in depth. Virtualization/Qubes, operating system DACLs, user space separation, network isolation, offline-only key management, the list is infinite! - monitor everything: network traffic pre-encryption, running processes, system calls, event logs, RF signals, sounds, power consumption, at the highest granularity possible. analyze what you monitor for anomalies and failures. (if you aren't watching, you won't know when you've caught something interesting, and/or need to harden some first line defenses) - custom build critical software components: kernel, crypto libs, secure applications (ssh,openvpn,etc), high risk browsers, email clients, chat clients, document viewers. (vast majority of exploits are tailored for common builds - if you build your own with custom configuration, suites, supported features, exploitation becomes a tailored and time consuming effort against your specific system) - employ camouflage to further thwart attempted attacks and increase the likelihood they'll be detected. look like WinXP but be a FreeBSD, claim to be Firefox with plugins such and such while actually running hardened chromium, spoof versions and platforms, etc. etc. - employ userspace entropy collection, hardware entropy sources, and strong entropy mixing across all applications, always! you may need libc hooking or dalvik interception to make built-in entropy sources not suck. (e.g. substrate for Android, LD_PRELOAD, etc.) entropy is a lucrative target, hard to verify, and often overlooked - make it a priority! - physical security is paramount: evil maid attacks, covert hw keyloggers, TEMPEST leaking cables. if they get their hands on it, it is pwned! (this may cramp your lifestyle) - operational security: don't even know where to begin with this one. bonus points for getting the fed chick[0] to take a bowl hit ;)
gh(who is now finally picking up the python language in a serious way)
excellent; i like Python quite a bit for many tasks, and you'll want to spend a week going through pypy/pip looking at useful modules. other languages on my short list: - C/C++ (it's everywhere. it will remain everywhere.) - Scheme/Lisp (for the perspective more than utility) - Ruby/PHP/PERL (good complements to Python. except PHP, which should be hated and ostracized :) - Bash/Csh/PowerShell (scripting++) - Go/C#/Java (you're going to want to know these sooner or later) what would you add, and why? best regards, 0. not trying to be a dick, but a dismissive chick label in this situation intentional. employing attractive women (or men?) to HUMINT targets may be par for the social engineering conference course, but subterfuge based in sexual wiles == cheap shots and disrespect. oh how hard i had to work to stifle a chuckle when $fed_chick explained she was "in desktop security but moving into laptops..." see also: "beware strangers with candy" best regards,
On 19 Jan 2014, at 9:59 , coderman <coderman@gmail.com> wrote:
0. not trying to be a dick, but a dismissive chick label in this situation intentional. employing attractive women (or men?) to HUMINT targets may be par for the social engineering conference course, but subterfuge based in sexual wiles == cheap shots and disrespect.
oh how hard i had to work to stifle a chuckle when $fed_chick explained she was "in desktop security but moving into laptops..."
see also: "beware strangers with candy”
Actually, for the feds that isn’t an entirely dumb idea, if their honey traps can’t manage to pretend to be delegates. Being so obviously fake, there’s a good chance that less paranoid delegates might assume she’s just trying to steal hardware from people who aren’t likely to want to report the circumstances (or trying her luck for a soon-to-be rich start-up king), and feel confident enough in their precautions to take that risk for a quick lay. (Of course, as demonstrated by numerous hacks at Blackhats many people aren’t paranoid enough even when they should be alerted to the heightened risk.)
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA384 Hey, On 01/18/2014 23:29, coderman wrote:
other languages on my short list: - C/C++ (it's everywhere. it will remain everywhere.) - Scheme/Lisp (for the perspective more than utility) - Ruby/PHP/PERL (good complements to Python. except PHP, which should be hated and ostracized :) - Bash/Csh/PowerShell (scripting++) - Go/C#/Java (you're going to want to know these sooner or later) what would you add, and why?
while it is nice to see that people are interesting in programming language where common bug classes of C and C++ are not present (read: no buffer overflows, format string exploits, no memory corruptions due to temporal safety (no double free etc.)). I suggest to look into http://media.ccc.de/browse/congress/2013/30C3_-_5412_-_en_-_saal_1_-_2013122... - -- which is about a compiler plugin to get rid of these bug classes in C (or any other language using LLVM). Still, we can do better. The rise of the Curry-Howard correspondence (programs and proofs are the same!) resulted in several programming languages whose type systems are so expressive that it can carry mathematical proofs (of intuitionistic logics) around. The common hello-world example is a list carrying (at compile time!) its length around, and thus being able to verify that append called on a list of length n and a list of length m returns a list of length n + m (and that reverse returns a list of the same length). While it is true, that these examples and languages are used mainly in computer science at the moment, I hope to see more people attracted to these kind of languages, writing libraries and applications. I can recommend several languages: - coq (http://coq.inria.fr) [the tutorial software foundations http://www.cis.upenn.edu/~bcpierce/sf/ ] - agda (http://wiki.portal.chalmers.se/agda/pmwiki.php) - idris (http://www.idris-lang.org/) There are certain tradeoffs and minor differences between those, I have the most hope with idris at the moment (due to design decisions from a practical point of view). In the end, I hope that the dream of (at least partially) verified systems will be reality during my lifetime, Hannes -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.19 (FreeBSD) iQIcBAEBCQAGBQJS3BUAAAoJELyJZYjffCjuF5MQALL5PqQyUYWH7TJQn6ZD3FwR vk/7OZwvlt2InHjFq1sx6mMp+k4/7Dc2Eb32rUPukU5NYIgmoIVGQz5rc3tTUUMH T8ttcjD8VP95Px26X3Gw3v9rD8QlWSUUdPtjC4IFK0lDhLmMzQDy49IPrh72XtEv GNZogxS29swhajhgh0UUieGoUnL55BafGnZoYu6j10OfY1qEsnLH++ISHM+G0HtS rOoi6dAlDW2wAj8Z6FopkWlTBuGjBeZD+csgg3y6r8LYRDKnl0KBcngdkHKjQ1UV UrqyYDiTOr2EG8ddYua7ZK756TdBDLVmsl5Er3KZFIaoY3D6QHvMbRd0NTNkSUJh yOqLS4RVlF22ztRKhn9oKTSyGRWRBIJCCPu7RPSHxs4fHJUfyRo1I2zI2RLaFNbU V5CYiS++EFgM+EyljcjoC5oYrjlEKA8lOAAgeaS0XJA1ViqnPo8BMsza50DLq7MS /MgWzSw8x43Ph4wjdeZwAH2XjM8Ek9SKXp+ojm61poYse2SWllfPyIZZOlDsAAgO Z0gjtZCFPVCEhoCTuSIULIJBQfcNkIoZw7feREwMYyV1bIdsOSjUC6bAIf6tmDB9 pkjO8jmyFC1B0GNeTBaLpIhcjdxtHz8xHi0f5U6uygt+pDZgCls7Xs3GgAWCoVHu e8+/2nfYpatyqDzmlkRh =Qz7b -----END PGP SIGNATURE-----
Hi Hannes! :) On Sun, Jan 19, 2014 at 06:10:08PM +0000, Hannes Mehnert wrote:
On 01/18/2014 23:29, coderman wrote:
other languages on my short list: - C/C++ (it's everywhere. it will remain everywhere.) - Scheme/Lisp (for the perspective more than utility) - Ruby/PHP/PERL (good complements to Python. except PHP, which should be hated and ostracized :) - Bash/Csh/PowerShell (scripting++) - Go/C#/Java (you're going to want to know these sooner or later) what would you add, and why?
while it is nice to see that people are interesting in programming language where common bug classes of C and C++ are not present (read: no buffer overflows, format string exploits, no memory corruptions due to temporal safety (no double free etc.)). I suggest to look into http://media.ccc.de/browse/congress/2013/30C3_-_5412_-_en_-_saal_1_-_2013122... - -- which is about a compiler plugin to get rid of these bug classes in C (or any other language using LLVM).
MPX was already committed to gcc trunk, so I hope this situation could improve in future (it is reverted for 4.9 but I think it will come back after the release in March). (I am still not sure how this will be rolled out, maybe by switching some software back to 32 bit to reduce the load on the pointer length lookup tables.)
The rise of the Curry-Howard correspondence (programs and proofs are the same!) resulted in several programming languages whose type systems are so expressive that it can carry mathematical proofs (of intuitionistic logics) around. The common hello-world example is a list carrying (at compile time!) its length around, and thus being able to verify that append called on a list of length n and a list of length m returns a list of length n + m (and that reverse returns a list of the same length).
While it is true, that these examples and languages are used mainly in computer science at the moment, I hope to see more people attracted to these kind of languages, writing libraries and applications.
I can recommend several languages: - coq (http://coq.inria.fr) [the tutorial software foundations http://www.cis.upenn.edu/~bcpierce/sf/ ] - agda (http://wiki.portal.chalmers.se/agda/pmwiki.php) - idris (http://www.idris-lang.org/)
Maybe you can comment a bit on the code extraction process into compilable languages. There seems to be a semantic differences between the proofable language and the language the extraction process targets in e.g. array handling(e.g. ocaml code) or just overflow handling in integers. I guess Idris does not have this problem? I always wondered if ats-lang would be the most suitable language for writing more typesafe code? Greetings, Hannes
[glossing over C and C++ lumped together; if there's one implementation that's seen exhaustive scrutiny, it would be Bitcoin in C++. only DJB can write C code without harm at every corner, however! ;] On Sun, Jan 19, 2014 at 10:43 AM, Hannes Frederic Sowa <hannes@stressinduktion.org> wrote:
... Maybe you can comment a bit on the code extraction process into compilable languages.
There seems to be a semantic differences between the proofable language and the language the extraction process targets in e.g. array handling(e.g. ocaml code) or just overflow handling in integers. I guess Idris does not have this problem?
I always wondered if ats-lang would be the most suitable language for writing more typesafe code?
thank you for these pointers, learning new things++ related efforts i've found interesting: Quark, ProofWeb, Frama-C, ELFbac, and interesting 30C3 presentation on "bug class genocide" http://www.youtube.com/watch?v=2ybcByjNlq8 best regards,
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA384 Hi, first of all I want to discuss 'verification'. There are so many different definitions and it seems everybody uses their own definition. It is strongly connected to trusted code base. Which axioms of a rule system do you believe in? Do you believe that arithmetic is verified? There are some axioms which you need to trust... [http://mathworld.wolfram.com/GoedelsIncompletenessTheorem.html] Some software 'verification systems' trust in more axioms than others... and yes, there have been verification systems which accepted invalid code/proved falsity. The other topic is trusted code base: - verification system itself (it's just a piece of software) - compiler? [http://cm.bell-labs.com/who/ken/trust.html] - language runtime? - operating system? - microcode of the processor? - hardware?? On 01/19/2014 18:43, Hannes Frederic Sowa wrote:
MPX was already committed to gcc trunk, so I hope this situation could improve in future (it is reverted for 4.9 but I think it will come back after the release in March).
The difference, as far as I can tell is in-band vs out-of-band signalling... (correct me if I'm wrong) with the former you put some magic values before and after the array, and an attacker has to guess these. The latter puts the meta-information out of band, hard to predict for an attacker.. that's at least the difference between the llvm bounds checks plugin (BoundsChecking.cpp / MemorySanitizer.cpp in LLVM 3.3) and the softboundCETS approach..
I can recommend several languages: - coq (http://coq.inria.fr) [the tutorial software foundations http://www.cis.upenn.edu/~bcpierce/sf/ ] - agda (http://wiki.portal.chalmers.se/agda/pmwiki.php) - idris (http://www.idris-lang.org/)
Maybe you can comment a bit on the code extraction process into compilable languages.
[I've to admit that I did some research in Coq over the recent 3 years (a higher-order separation logic to verify the full functional correctness of Java programs). And no, at the moment I don't believe anymore in taking off-the-shelf code and verify its correctness. That's a myth. If we need to reimplement it anyways, why not in a neat modern programming language?] In Coq you can develop programs and extract them to ML code, without the irrelevant proof bits. But it seems this is rather cumbersome. The verified optimizing compiler for C, compcert [http://compcert.inria.fr/] does this. The softbound plugin [http://acg.cis.upenn.edu/softbound/], although they developed a semantics for the LLVM intermediate representation, have the real implementation in C++ and no formalized proof (at least I couldn't find any) of its correspondence to the Coq development. I actually think there are some overflows in the C++ runtime (size + start < bound might fail The verified L4 microkernel redeveloped a bunch of C++ and assembly into Haskell in order to be able to prove it. The main difference between Coq and Agda/Idris is that the dependent types are used in Coq to proof stuff, while in Agda/Idris you use them for programming. (Obviously, all is the same, and Adam wrote a great book about programming with dependent types in Coq http://adam.chlipala.net/cpdt/). Agda has a story about people not interested in executing programs, but rather type check and prove them. Idris has a slightly different tradeoff -- instead of forcing developers to write only total functions (due to curry-howard, partial functions better not be used for proofs [basically if you use a partial function for a proof, you assume false, and can prove everything]), but also partial functions. Only total ones can be used for proving though. Idris has a compiler which produces executable programs! :) Obviously the runtime needs to be looked into. In the end it is part of your trusted code base. Unfortunately I have not used ATS, but if I'm not entirely wrong, it is a dependently typed programming language with mutable state and a C foreign function interface which treats variables as resources (and uses linear logic/linear types to do so). A very interesting system; Chris Double wrote several blog posts when he used it http://bluishcoder.co.nz/tags/ats/ . I'm happy to discuss further, Hannes -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.19 (FreeBSD) iQIcBAEBCQAGBQJS3Q4iAAoJELyJZYjffCjuuwAQAIlV480onmDrunNB5GOrRqXK EaEfbIQPRZT4tnaj9zrqjxAxgh+gls9ugKPKPaUfQzxzQUPSn88SWx6dpRKfGYZu e4N77kSCb1YoTnG9SjWao2IVRxnSZXtATmNAEQG8FqyXejbq+G1IJfP2eX9DRzM8 nLB1JQLWcI4lZonYYh2pIHA8n0raJav2OCqUhp7tbjEuubU2Uxil8ToHDMfaqzSY /hanRu/F9sCFVNtNOysIsbP8bUukZLex3yIgRIiojUy3S2872doqSL1QNeRa3A/Z aOifWowLi4UdCdcmk2obvdI4sSanh7LG5ijw9IZDXdOsWM4Jyb9qZS+PP0Rs6I6T IzHwA5wf+Te0q6Gh621W6bDnaR4dDd6cARmLafyGyY0ViRbWJoLjLW6d4zfXttvh V/dryq4LjdztlyblfjxY9Djlx2O8JO/Q7/YYhb8ZpOn8lek7cQH4FxZWGmWqpiEf Ay7A1nPM47BIPgKgTFRdMpeUnrttm+HMXOHtx9sID6jycT8HsJxOA645gunhi4D+ 5UhcKMNUZae2tiqxOeUsvxI9/YwZu7g2FLvgoR4h7koQfl1jpsbNxE2ckopc+2ej 1YQDF7ZB0gTXyX9xHRxSEb76fFBW1sPz0s/W5DTEnQw+DnT0LIXaNGsvzAE7RU/e GcMkqEodPLluzQJgPwz4 =xZP7 -----END PGP SIGNATURE-----
Hi! On Mon, Jan 20, 2014 at 11:53:06AM +0000, Hannes Mehnert wrote:
[...]
On 01/19/2014 18:43, Hannes Frederic Sowa wrote:
MPX was already committed to gcc trunk, so I hope this situation could improve in future (it is reverted for 4.9 but I think it will come back after the release in March).
The difference, as far as I can tell is in-band vs out-of-band signalling... (correct me if I'm wrong) with the former you put some magic values before and after the array, and an attacker has to guess these. The latter puts the meta-information out of band, hard to predict for an attacker.. that's at least the difference between the llvm bounds checks plugin (BoundsChecking.cpp / MemorySanitizer.cpp in LLVM 3.3) and the softboundCETS approach..
MPX uses CPU managed out-of-band (but in application memory) page-table-alike structures to store the bound table entries. They get updated via specific cpu instructions, which result in nops on todays cpus (so you can execute mpx code on non-mpx cpus and just won't have the bounds checking). They also made sure that non-MPX code that is linked against MPX code can propagate unbounded pointers, so you don't need to switch your whole operating system to MPX enabled code at once (I guess that would aslo be a problem memory-wise, but Intel entered the DRAM business again, too :) ). The x64 linux ABI has also been updated. While passing parameters and returning, MPX will introduce new registers to pass those bounds checks automatically between function calls. I guess this enables faster function calls because the cpu does not need to store those pointer bounds in the permanent pointer bound tables thus eliminating the stress on the cpu caches. You can find details here: <http://download-software.intel.com/sites/default/files/319433-015.pdf> What would be interesting, especially for the linux kernel, is to restrict jmp and callq addresses so it is impossible for an attacker to get control over them and e.g. dispatch own code on network packet dismantling without needing whole pointer checking infrastructure e.g.
I can recommend several languages: - coq (http://coq.inria.fr) [the tutorial software foundations http://www.cis.upenn.edu/~bcpierce/sf/ ] - agda (http://wiki.portal.chalmers.se/agda/pmwiki.php) - idris (http://www.idris-lang.org/)
Maybe you can comment a bit on the code extraction process into compilable languages.
[...]
The softbound plugin [http://acg.cis.upenn.edu/softbound/], although they developed a semantics for the LLVM intermediate representation, have the real implementation in C++ and no formalized proof (at least I couldn't find any) of its correspondence to the Coq development. I actually think there are some overflows in the C++ runtime (size + start < bound might fail
IIRC this was already addressed in the talk.
The verified L4 microkernel redeveloped a bunch of C++ and assembly into Haskell in order to be able to prove it.
The main difference between Coq and Agda/Idris is that the dependent types are used in Coq to proof stuff, while in Agda/Idris you use them for programming. (Obviously, all is the same, and Adam wrote a great book about programming with dependent types in Coq http://adam.chlipala.net/cpdt/).
I would also like to point to Software Foundations from Benjamin Pierce here, as it also has some great material to learn Coq: <http://www.cis.upenn.edu/~bcpierce/sf/>
Agda has a story about people not interested in executing programs, but rather type check and prove them.
:)
Obviously the runtime needs to be looked into. In the end it is part of your trusted code base.
Code generation without heavy runtime would also be nice.
Unfortunately I have not used ATS, but if I'm not entirely wrong, it is a dependently typed programming language with mutable state and a C foreign function interface which treats variables as resources (and uses linear logic/linear types to do so). A very interesting system; Chris Double wrote several blog posts when he used it http://bluishcoder.co.nz/tags/ats/ .
ATS uses plain C as an intermediate language and the whole language feels pretty low-level, too. So it seems it is easily possible to compile these programs freestanding and also link those to other programs, which is quite a nice feature, especially if one wants to make incrementally use of more checked languages. Thanks for your additional remarks, Hannes
On Mon, Jan 20, 2014 at 02:42:34PM +0100, Hannes Frederic Sowa wrote:
What would be interesting, especially for the linux kernel, is to restrict jmp and callq addresses so it is impossible for an attacker to get control over them and e.g. dispatch own code on network packet dismantling without needing whole pointer checking infrastructure e.g.
Just remembered there was some research on this already: <http://zero-entropy.de/fpp.pdf> Greetings, Hannes
On Sat, Jan 18, 2014 at 12:16:45PM -0800, gwen hastings wrote:
we should just stop using loaded language like "NSA Proof" and resting on past laurels to assure folks that such is a fact(it isn't).
proof implies 100% security. eh? we all know that that's a unicorn.
gh(who is now finally picking up the python language in a serious way)
<3 hell yeah, it sometimes pays to be grumpy.
next will be taking pbp routines and formats and creating a new curvep25519 version of type 1 and type 2 remailers with a nym.alias.net clone in python using Curvep25519 keys to emulate a type 1 reply block(have to see what mixminion does for reply-blocks if any)
fantastic. just 2 days ago i hacked an AMM together using pbp. https://www.ctrlc.hu/~stef/amm.py - proper release coming soon. should be hosted on an .onion address.
ps2ps: PCP and PBP developers need to make up their collective heads about external representation key formats for public keys(I will be using pbp as its already in python)
we are off-list in fruitful contact.
I am kind of dependent on these(key format representations)
pbp is still kinda experimental. but the more users and the more feedback on key-formats and related stuff gets us faster to stability. nb: your pgp key is kinda huge due to the embedded jpg of yours, which is kinda contra-productive, it does not allow visual recognition, but leaks side-chan information that could be used against you. -- pgp: https://www.ctrlc.hu/~stef/stef.gpg pgp fp: FD52 DABD 5224 7F9C 63C6 3C12 FC97 D29F CA05 57EF otr fp: https://www.ctrlc.hu/~stef/otr.txt
participants (9)
-
coderman -
gwen hastings -
Hannes Frederic Sowa -
Hannes Mehnert -
Jim Bell -
Lance Cottrell -
Philip Shaw -
Sam Gordon -
stef