August 2013 - cypherpunks - lists.cpunks.org

[Cryptography] The Case for Formal Verification
by Eugen Leitl 30 Aug '13

30 Aug '13

----- Forwarded message from "Perry E. Metzger" <perry(a)piermont.com> ----- Date: Thu, 29 Aug 2013 16:46:30 -0400 From: "Perry E. Metzger" <perry(a)piermont.com> To: cryptography(a)metzdowd.com Subject: [Cryptography] The Case for Formal Verification X-Mailer: Claws Mail 3.9.0 (GTK+ 2.24.20; x86_64-apple-darwin12.4.0) Taking a break from our discussion of new privacy enhancing protocols, I thought I'd share something I've been mumbling about in various private groups for a while. This is almost 100% on the security side of things, and almost 0% on the cryptography side of things. It is long, but I promise that I think it is interesting to people doing security work. When I was a student the first time, in the early to mid 1980s, formal verification was clearly a dead end that would never get anywhere. A boss of mine once asserted (circa 1988) that there would never be a verified program that did anything terribly interesting, and at time he seemed right. Today, there is a formally verified microkernel called seL4, a formally verified C compiler called CompCert, a formally verified experimental web browser called Quark, and lots of other stuff, much of which I doubtless don't even know about. _Things have changed_. Much of what has changed is proof technology, and it is a technology. The tools for doing formal verification are now, for the first time, just barely usable for real work on interesting programs, and getting better all the time. Over the last twenty five years, we figured out a lot of stuff people didn't know before about how to write verification tools and how to verify programs, and the results have been impressive. There are usually several arguments against formal verification: 1) We don't know what to specify, so what help does proving a buggy specification do us? 2) Who would bother writing a proof vastly larger than their program? 3) You can't prove programs of interesting size anyway. So, taking these in reverse order: For 3 ("you can't prove anything big enough to be useful!"), the Quark project: http://goto.ucsd.edu/quark/ showed you don't need to prove a program of interesting size. You can defend millions of lines of buggy code with a "software firewall" made of formally verified code. Verify the right thousand lines of code that the rest needs to use to talk to anything else, and you have very strong security properties for the rest of the code. seL4 and CompCert are clearly also quite useful programs. For 2 ("Who would bother with all that work?"), we have libraries in daily use like sqlite: https://www.sqlite.org/testing.html where the system has a fairly small amount of production code and literally 1000 times more lines of test code than production code. If you're willing to write ninety million lines of test to defend ninety thousand lines of code, formal verification is totally doable. Sure, it might not be worth it for throw away code or for your new video game or conference room scheduler where failure isn't a big deal, but it is *very* clear why you would want to do this for foundational code of all sorts. For 1 ("We'll never write a correct spec anyway, so what good is the proof?"), I think we've been suffering from sour grapes. We didn't have the ability to prove big things anyway, so why not tell ourselves that there's nothing interesting and large we could prove that would be worth proving? CompCert is a fine counterexample, a formally verified C compiler: http://compcert.inria.fr/ It works by having a formal spec for C, and a formal spec for the machine language output. The theorem they prove is that the compilation process preserves observational equivalence between the behavior of the C program and the output, which, given correct notation, is a very small theorem to write down. You might claim "so what, it is probably actually buggy as hell, the spec probably isn't really correct anyway, etc." -- except when John Regehr's group built tools to torture test C compilers, the only compiler they did *not* find bugs in was CompCert. They found hundreds of bugs each in every other compiler tested. (They actually found one, but arguably it was a bug in a Linux include file, not in the CompCert compiler.) Similarly, one might claim "there is no way to formally specify a web browser that won't be just as buggy as the web browser!", but Quark's formal verification doesn't try to show that the entire Web browser is correct, and doesn't need to -- it shows that some insecure behaviors are simply impossible. *Those* are much simpler to describe. Certainly there may be other properties that turn out to be important that no one has considered yet. However, unlike testing, if people discovered a hole in the set of theorems being proven -- some property that was important but which had not been considered -- then that could be added to what was proved, and _then the problem would be gone forever_. Verification means you get actual incremental progress that you can trust. Testing is much less powerful. (Furthermore, future systems can learn from what you did and add the needed theorem to what they prove about their own system.) I don't think the technology is up to proving huge systems correct -- a fairly unambitious C compiler or a microkernel is the current limit -- but it is up to proving the right thousand lines of code here and there without much fuss, and that might make an incredible difference in systems security if people actually take it seriously. So, if you're interested, how do you get started doing such things? At the moment, the best system for doing this sort of work is Coq: http://coq.inria.fr/ Coq is sort of a programming language (although it is not quite Turing equivalent -- all programs must be guaranteed to terminate for technical reasons), sort of a form of constructivist logic (i.e. all existence proofs construct examples, no law of the excluded middle). It uses a neat trick called the Curry-Howard isomorphism that may take some getting used to for people not exposed to modern type theory. In it, types and logical propositions are the same thing, and programs and proofs are the same thing. You can write a function that adds two numbers, or a function that proves that there are an infinite number of primes. The type of the former is clearly an integer, but the type of the latter is the theorem itself. A proof that proposition A implies proposition B is function of type A -> B -- any function that takes a proof of A and yields a proof of B is after all a proof that if A is true then B is true. (This is why all functions in Coq itself must terminate -- otherwise all types would be inhabited so all theorems would be true. That in no way restricts one's ability to build verified non-terminating programs using the system, you just have to build them by reasoning about programs that Coq itself can't execute.) Proofs in Coq are generally not written by hand, though. Instead one uses a sublanguage called the "tactic language" in which one invokes help from Coq to interactively assemble a proof, which makes doing the proof far easier. For many theorems, you can almost completely automate the proof, while for others, you need to help Coq along more. (Some of the tactics are quite amazing, "Omega" for example will prove any assertion about numbers that does not involve multiplication by a variable, aka "Presburger arithmetic".) Often, one builds software using Coq by constructing a sort of formally verified assertion about what the program would do, and then using a built in Coq facility to mechanically extract that into a working verified program written in OCaml, Haskell or Scheme. Nothing in theory prevents you from doing things many in other ways, though -- the system is quite general. Coq is, sadly, needlessly hard for the beginner. It has poor documentation, bad error messages and bad error behavior. These are not inherent problems, they're problems just with this instance of things -- people could build better if there was enough interest, and I hope that as these technologies become more popular people will build far better versions of the tools. However, bad documentation or no, at the moment, this is the right place to go I think. It is the system Quark and CompCert were built in, and not by accident. It is not for the faint of heart -- the learning curve is very steep. Still, it is quite doable. The right places to start with Coq are probably Benjamin Pierce's online Software Foundations textbook: http://www.cis.upenn.edu/~bcpierce/sf/ and, when one is done with that, possibly Adam Chlipala's online book "Certified Programming with Dependent Types" http://adam.chlipala.net/cpdt/ (There's also a manual for the system itself, as well as this book on Coq: https://www.springer.com/computer/swe/book/978-3-540-20854-9 ) I'm happy to give help to anyone trying to learn how to do this sort of thing -- we need more people in the world experimenting with verification if we're going to get truly trustworthy software going forward. Let me assert that we *do* need truly trustworthy software, too. We've been very, very good for years now at finding hole after hole in running code and making the systems we depend on every day into a minefield that we dare not take an unconsidered step in. Wouldn't it be nice to make some progress in the other direction? Perry -- Perry E. Metzger perry(a)piermont.com _______________________________________________ The cryptography mailing list cryptography(a)metzdowd.com http://www.metzdowd.com/mailman/listinfo/cryptography ----- End forwarded message ----- -- Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org ______________________________________________________________ ICBM: 48.07100, 11.36820 http://ativel.com http://postbiota.org AC894EC5: 38A5 5F46 A4FF 59B8 336B 47EE F46E 3489 AC89 4EC5

2 1

[cypherpunks] Signed vCards
by DataPacRat 30 Aug '13

30 Aug '13

I've just submitted the first draft of an Internet-Draft to the IETF. If it makes it through the whole editing process, it will take an existing file format used for identity-description, and adds a few details to allow crypto algorithms to be used for identity-/assertion/. It may not seem like much, but it could improve some aspects of hierarchical certificate authorities, encrypted email, and suchlike. It’s the most important thing I think I’ve been able to work on in the last little while, and I hope the editing process goes well. ---------- Forwarded message ---------- From: <internet-drafts(a)ietf.org> Date: Fri, Aug 30, 2013 at 3:33 AM Subject: New Version Notification for draft-boese-vcarddav-signedvcard-00.txt To: Daniel Eliot Boese <datapacrat(a)datapacrat.com> A new version of I-D, draft-boese-vcarddav-signedvcard-00.txt has been successfully submitted by Daniel Eliot Boese and posted to the IETF repository. Filename: draft-boese-vcarddav-signedvcard Revision: 00 Title: vCard Format Extensions : Signed vCards Creation date: 2013-08-30 Group: Individual Submission Number of pages: 11 URL: http://www.ietf.org/internet-drafts/draft-boese-vcarddav-signedvcard-00.txt Status: http://datatracker.ietf.org/doc/draft-boese-vcarddav-signedvcard Htmlized: http://tools.ietf.org/html/draft-boese-vcarddav-signedvcard-00 Abstract: The base vCard 4.0 specification defines a large number of properties. This specification adds two new parameters and six new properties to vCard 4.0, which allow the use of cryptography and public-key infrastructure (PKI) for identity assertion. Note Discussion and suggestions for improvement are requested, and should be sent to vcarddav(a)ietf.org. Please note that it may take a couple of minutes from the time of submission until the htmlized version and diff are available at tools.ietf.org. The IETF Secretariat Thank you for your time, -- DataPacRat "Then again, I could be wrong."

1 0

UDP/datagram/cell based networks [was: Why_can't_email_be_secure]
by grarpamp 30 Aug '13

30 Aug '13

On 8/26/13, coderman <coderman(a)gmail.com> wrote: > On Sun, Aug 25, 2013 at 10:52 PM, Bill Stewart <bill.stewart(a)pobox.com> >> Datagrams don't give you any useful anonymity, > ... > usability for example to support UDP traffic and applications which Are we necessarily even speaking strictly of UDP 'datagrams' or applications? For example, I presume there might be something to be said for software switched packet/cell network stacks. Even if they are encapsulated in meshes of TCP overlay circuits for the TCP properties. Streams of buckets passing inside, be they full of ham or discarded chaff. The cost is the bandwidth you wish to dedicate to it, the cpu/ram to pass, route and control it. Can old ATM transports be anonymized or assist in that...

2 4

WaPo on "$52.6 billion 'black budget' for FY2013"
by Gregory Foster 29 Aug '13

29 Aug '13

Washington Post (Aug 29) - "U.S. spy network’s successes, failures and objectives detailed in ‘black budget’ summary" by @BartonGellman & @gregpmiller: http://www.washingtonpost.com/world/national-security/black-budget-summary-… gf -- Gregory Foster || gfoster(a)entersection.org @gregoryfoster <> http://entersection.com/

1 0

[liberationtech] Videre: the secretive group on a mission to film human-rights abuses
by Eugen Leitl 29 Aug '13

29 Aug '13

----- Forwarded message from catchalladdress(a)nym.hush.com ----- Date: Thu, 29 Aug 2013 15:01:14 +0100 From: catchalladdress(a)nym.hush.com To: liberationtech(a)lists.stanford.edu Subject: [liberationtech] Videre: the secretive group on a mission to film human-rights abuses Reply-To: liberationtech <liberationtech(a)lists.stanford.edu> http://www.wired.co.uk/magazine/archive/2013/09/features/videre Somewhere in Africa, a white man gets up and goes to the bathroom. He pops up the handle on his wheeled suitcase and pulls it across the tiled floor and down a set of steps to the urinal. When he has finished he hauls the case back up the steps to the table and parks it beside him, within arm's reach. He never lets the object out of his sight. The bag is his life, and it exercises power over many other lives too. If it fell into the wrong hands there would be consequences -- the contents could cause people to be tortured, or even murdered. That's why Wired cannot tell you where he is sitting, nor reveal his identity. Nor can we reveal the country -- except to say that it's outside Africa -- where he lives with his family. His wife exists in a state of anxiety when he is not at home and is often irritated when he is, such are the distractions of his work -- notably the constant interruptions of his nine phones. She is proud of his work, he says, but angry too. The pair are in counselling. The phones ring at all hours of the day and night. Often the person on the other end of the line is thousands of kilometres away, in fear of his or her life, with no one else to turn to. At that moment, the man needs to make a decision -- to offer advice or direction that could make the difference between life and death. He does not carry that burden lightly. The man must remain anonymous and, for this story, he has asked to be known as Carlos. He says that he was brought up in Romania, and that he served in the army. He is in his thirties, slightly built, and has a beard to make himself look older. We meet in the spring of 2013 at an airport in Africa. He asks not to be referred to by name in front of anyone else, especially colleagues, who know him by different names. Carlos's colleague, Oren Yakobovich (his real name), arrives soon afterwards. Yakobovich, 42, is a former Israeli soldier who still carries himself with a military bearing. He picks up a hire car and drives us through the city, moving slowly in the early-morning traffic, and head for the suburbs, to the group's regional office. He repeatedly checks the rear-view mirror. "We're not being followed, that's for sure," he says. The secrecy is for good reason: Yakobovich and Carlos operate a ground-breaking human- rights organisation that uses video footage -- obtained both openly and covertly using hidden cameras -- to tell the stories of people suffering at the hands of oppressive, violent regimes. After operating in almost total secrecy for the last three years, the two men have offered wired unprecedented access to the work of their organisation, Videre. The NGO's name comes from the Latin "Videre est credere", which means "to see is to believe". Its mission is to reveal the workings of violent regimes through a network of activists who film and record abuses and violations of human rights. When necessary, its operatives film secretly, tracking the activities of tyrannical rulers and their cronies like an intelligence service. It operates in several African countries and has a substantial presence in one particular troubled nation where state terror and violence are widespread. Videre taps into a network of 120 human rights workers (referred to as "researchers") in that country who film -- some of them at enormous personal risk -- the activities of the state security services and their political masters, in some circumstances undercover. Each group operates in a cell structure. "It's a bit like the network of Al-Qaeda," Carlos explains, and then wonders at the wisdom of likening his organisation to the world's most notorious terrorist organisation. Another parallel is the Provisional IRA, which organised its operatives in small groups so each was unaware of what the others were up to -- no individual could give the others away if caught. As head of operations, Carlos feels personally responsible for the researchers, as well as the other volunteers and paid staff who support them. He shuttles back and forth on long-haul flights between hot spots in Africa, his family and Videre's headquarters in London. He explains that he's anxious on planes. It's not fear of flying, but the thought that, while he's in the air, someone in his network will be in trouble and he won't be available to help them. He describes a walk he takes at his home airport from the plane to passport control: a walk between one world and another. "I often used to cry on that walk, for the tensions, for the things I've heard," he says. Last spring, one activist was caught filming by the security services of the oppressive regime in question. This led to another arrest and a Videre operative being subject to torture and violent interrogation. He was coerced into revealing information about the organisation. Carlos has since learned that the security services already knew about him, although they are familiar with only one of his aliases, and not his real name. Yakobovich argues that some of the human rights workers are less at risk with cameras as the authorities know that reprisals will be recorded. However, some activists are targeted by the authorities, and some have been captured while filming. Because of this, Carlos and others are constantly trying to make the cameras more discreet, but without sacrificing their effectiveness. (Those pictured in this story are all discontinued.) The devices need to be simple and easy to use by people in vulnerable circumstances who may not be adept at surveillance or familiar with technology. Secret filming devices formerly used by VidereLiam Sharp Carlos has come to show some of the lead researchers the most recent hidden-camera designs he's been working on. Videre's covert operatives largely use Chinese-made spy cameras that resemble memory sticks. Each has a small, rechargeable battery and records on to SD cards. The devices can be clipped into shirt pockets, but the camera lenses must be visible in order for them to be able to function effectively, which exposes some operatives to danger. The African state in question knows it is being watched. Political activists and militia members have delivered stark warnings. Those attending a rally were recently told: "It is a political meeting. Is that clear? It's a family affair. No one should record what's happening here because it's an internal matter. If we catch you recording us, you will be [in] trouble." Carlos has been hacking the Chinese spy cameras -- he tears them apart and uses the components in his prototypes. When he and the researchers are happy with a design, they produce it in bulk. He once made a chunky, rubberised crucifix with a camera sealed inside. At the centre of the cross was a pinhole lens. The device was dismissed as bulky and conspicuous. Carlos has built new iterations -- prototypes have been brought to Africa for consideration by operatives who have travelled to meet him in a neighbouring country's capital. It's an 18-hour journey on a crowded bus with long delays at the border. Tonight, in darkness, Carlos and Yakobovich will cross the city -- observing counter- surveillance routines designed to thwart anyone following them -- to a secret destination where they will meet the researchers. Videre was founded in 2008 by two Israelis who, unknown to each other, had the same idea at a similar time. Yakobovich was raised in a right-wing Israeli community near Tel Aviv. As a youth he readily accepted the status quo of fervent Israeli nationalism. "The Arabs did not exist, they were there but they had no rights and didn't deserve a country," he says, explaining his former views, over coffee and hummus in a Marylebone hotel, before the trip to Africa. He couldn't wait to join the army. He was so enthusiastic about conscription that he began training before he started, working on his fitness so he would be a better soldier. He was quickly promoted to officer. "I had more power at 19 than I ever had in my whole life before or since," he explains. "It gives you great skills for life." Serving in Gaza, he says that he was never close enough to confirm a kill, but he certainly shot people. "You're up on the Lebanon border, there are terrorists coming, you're going in, you start shooting…" he says. Mostly, though, he was involved in gathering intelligence. There was no single terrible incident or atrocity that made him become disillusioned about the Israeli cause or the way the army treated the Arabs. But he became gradually aware that his involvement in day-to-day activities, such as checking men, women and children at checkpoints, was creating more hate, more enemies -- and probably more terrorism too. He says his fellow soldiers thought of all Arabs as potential enemies, and treated them accordingly. He noted how ordinary young Israelis could switch from compassion to cruelty. "I gradually realised there was something very wrong," he says. Finally, he refused to go to the West Bank on a guard detail. He was supposed to be protecting a secret counterterrorist mission, and disobeying an order made him a refusenik. He says he spent a month in jail. "I didn't want to do it any more," he says of the military. Because he was an officer the conditions in prison were tolerable. He infuriated the prison authorities by climbing on the roof to salute supporters of the refuseniks on a nearby hill. "But no one abused me or beat me -- there was time to think," he says. Videre footage of citizens and security forces, filmed in an unnamed terror-state in Africa Having served his time, he was released from the army and, increasingly aware of the social and political troubles in Israel, decided to become a film maker. He thought he could change the world, but also meet girls. "I thought it was a very cool thing to do... always better than saying you're a banker," he says. He never went to film school -- he couldn't afford it -- so he took out a loan, bought a camera and started filming, making a series of documentaries in the early 2000s that he hoped would stir Israeli sentiment. There was a film about the Bedouin, another about education for Palestinians, another about the treatment of psychiatric patients. He met women too, but nothing really changed and he became disillusioned with the insular world of film festivals and screenings. In 2005, out of frustration and hope, Yakobovich joined the Israeli human-rights group B'Tselem and gave the organisation's work new impetus by setting up a video unit and supplying cameras to families living in areas where they were facing daily conflict with settlers. The Palestinians filmed openly, not needing to use secret cameras. (Yakobovich later -- wrongly -- assumed the same approach would be possible in Africa too.) One sequence, from 2007, became notorious in Israel, and was also broadcast on the BBC and CNN. At a Hebron home that became known as "the cage house", a Palestinian family found itself under verbal attack from settlers. One of them - - a 16-year-old girl -- filmed herself being abused by an Israeli woman, who called the teenager a whore. "Sharmuta Video" - Settler harassment of Palestinians in Hebronbtselem "I think it was very shocking for people to see these words coming from a very religious woman," says Yakobovich, who remains a firm believer in Israel. "And what was even more shocking was two soldiers standing there doing nothing to protect the young girl. They are supposed to be a moral army." Yakobovich's work generated hate mail and death threats, but he believes it made a substantial difference by helping to reduce violence towards Palestinians in the West Bank. "My strongest belief in the human-rights struggle is you don't have a big fight, you don't have big wins," he says. "It's the small, uphill battles, the small wins that bring about change over time." He started to wonder if the same model might make an impact further afield. Around the same time, Uri Fruchtmann was thinking along similar lines. Fruchtmann, who chairs Videre's Board of Trustees, has followed an unlikely path to human-rights work: a successful entertainment executive, he has produced several films, among them Spice World, featuring the Spice Girls. For 12 years he was married to Annie Lennox, with whom he has two children. Fruchtmann, 58, is a reflective, easy-going character with powerful connections. ( Brian Eno -- a friend -- hosted a fund-raising party at his studio in the early days of Videre.) It was through a conversation with another friend, Terry Gilliam, now a Videre board member, that Fruchtmann had the idea of exploiting the rapid obsolescence of equipment in the film industry by buying up old cameras, so that they could be used to record human-rights abuses. In the 90s, he had been involved in an environmental campaign in Majorca where he had helped to make a short film explaining the plight of the black vulture. The film had raised significant funds for the cause and made Fruchtmann consider the potential of film as a weapon for human-rights work. Like Yakobovich, Fruchtmann had made trouble during his own time serving in the Israeli army. He had been a conscientious objector in the 70s and had been beaten up by his fellow soldiers for not observing the rules. According to Fruchtmann, he was called before a military court eight times -- each occasion led to another month in jail. "I always had a passion for justice, or a passion against injustice," he says, in a restaurant near London's Baker Street in May. His parents fled Nazi Germany, losing everything. After the army, Fruchtmann became a hippy and travelled round Europe, then worked as a photographer in Israel; eventually, like Yakobovich, he became a documentary maker -- making two music films, Stir It Up and The Atlantic Records Story, both released in 1994 -- before producing his first feature, Spice World, in 1997. He now co-owns Ealing Studios. Neither Fruchtmann nor Yakobovich can remember how they met. Fruchtmann travelled to the West Bank in 2008 looking for partners for his project. "People told me I should talk to Oren," he says. "We found each other and went around the West Bank together." Fruchtmann recalls the filming of the 1991 beating of Rodney King as a defining moment on the journey to Videre. King, an African- American, was attacked by five police officers in Los Angeles. As they assaulted King with their batons, they were filmed by a local resident. The footage was transmitted around the world. When the officers were acquitted, there was widespread rioting. Fruchtmann wondered: if every parking violation is being recorded on film, why shouldn't human-rights abuses be recorded? He describes the approach as "little brother turning the cameras on Big Brother". "I was forced to dance with a man I didn't know. He said he was my husband for the day. They asked me how it felt. I said it was nice as I felt I had no choice. I don't even recall the rest who raped me afterwards." Several staff in Videre's regional office sit at screens reviewing video footage. Onscreen, ten women who live in a state we can't name, describe multiple rapes and terrible violence they suffered at the hands of 25 men. They did not know all of their attackers, but some still lived in the same communities. One woman speaks of remembering how a local politician had urged the men to assault her. "They randomly took us and shared us among themselves... they only finished at dawn," she says. "I was forced to dance with a man I didn't know. He said he was my husband for the day. They asked me how it felt. I said it was nice as I felt I had no choice. I don't even recall the rest who raped me afterwards." One woman was pregnant when the men came looking for her husband. He escaped. "I pleaded for mercy -- they said they didn't care, it's politics," she says. "After the lashes, I started bleeding, then passed out." She says she was repeatedly raped while unconscious. "Later I heard them say it was a boy. I had a miscarriage. [A villager] took away my baby. I didn't even know where they dumped it." The woman discovered she was HIV positive. Ashamed to tell her husband what had happened, she infected him. She went to the police to report the rape but "they clapped their hands and laughed". The women are speaking because they want the perpetrators brought to justice. Videre has used trusted local contacts to identify the victims and build confidence among them that it is safe to talk. One day, Videre hopes, there will be criminal trials. The woman who miscarried says: "It's for us to live with the culprits, they are still tormenting us." Data-mining software creates patterns and networks of rights violations by combing the web and Videre footage Videre has set up the office in the city of the neutral African country as a place to collect, process and distribute the footage its researchers obtain from the terror state. It's smuggled into the country by Videre operatives riding buses. One of the three full-time office staff, Eddie (not his real name), meets the couriers at the bus terminal, often not knowing who they are or how to find them. "There are always problems collecting the film," says Eddie, a bullish, articulate young white man. He sometimes has smooth handovers, where a hard drive is handed over concealed inside a newspaper or collected from a dead letter drop but, more often than not, the courier gets lost, or their phone is dead after the long bus journey. The Videre staffer will roam the bus station, sometimes on the phone to Carlos in another continent, trying to identify the courier. The Videre office workers know the couriers and researchers only by code names: Carlos alone knows their real identities and choreographs the entire operation by phone, email and Skype when he is away. Every communication is encrypted. Carlos uses HushMail and Tor. TrueCrypt encrypts and disguises files and can also protect hard drives. If a hard drive is encrypted and is connected to a computer that doesn't use TrueCrypt, one click will erase the material forever. Footage is recorded on SD cards and copied on to hard drives in the country of origin, where it is disguised as an MP3 or .mov file and encrypted. The office contains powerful servers that are stored in a walk-in safe. The footage is retrieved from the hard drives before being archived and catalogued using CatDV software. There may be many hours of tedious, useless footage to screen before there is anything worth showing to the world. But if Videre is lucky, some footage will be of usable quality. All too often the image is good but the sound quality poor, or it's the other way around. "We have footage of a body in the morgue, beaten, shot -- you can see bullets still in his body" Mike The archivist, Sonia (not her real name), is a young woman whose family comes from the terror state. Her father has been imprisoned and her uncle was killed by political rivals. For her the material has special relevance. "I don't just watch the footage, I become the footage," she says. "We never know who filmed it, I always imagine it could be my own father or cousin." She is unable to tell family or friends the nature of her work. It's like gold mining, she explains: you might sift through 40 hours to find a single nugget. She and her colleagues give feedback to Carlos, who passes it on to the researchers in the hope they will supply better footage. Sonia's colleague Mike (not his real name) edits the footage for distribution. He too is from the terror state and says that watching the film can be both depressing and absorbing. Much of the footage comes from remote areas where abuses and violations are commonplace. The perpetrators believe they can act with impunity as they are far from international journalists. Some researchers are becoming increasingly bold, filming in prisons, morgues and open-air rallies where intimidation and the threat of violence prevail. "We have footage of a body in the morgue, beaten, shot -- you can see bullets still in his body," Mike says. "He was a working on a farm where the owners are mistreating the employees -- and this visual brought the story together." Mike recently returned to his home country, intending to do some filming at a political rally. "But I lost courage and missed the action because I was so scared. In the end I had to hide behind a truck and start filming." He can't think of anything as brave as the researchers risking their lives. "It makes me sad, man, that something has broken down in African society," he says. "We are known for hospitality, for community. We rotate during the famine -- today the whole village comes to my field, tomorrow to yours. Now people are killing and harming each other because of politics." One of Videre's film packages highlights the politicisation of food, in which supporters of the main party are given sacks of seed as staple foodstuffs, and opponents are denied food altogether. "The ethos is not to shock but to effect change and we try to avoid the usual African stereotypes, the diet of violence" Eddie There is significant emphasis placed on verification of the footage. The context is analysed, as is the metadata, which is relayed to a team on the ground which then undertakes further checks. Translation is done by more than one person to ensure that all the nuances of the language used in the clips are understood. If there is any doubt as to the veracity of the material, it won't be released. Once it has been edited, Videre's footage is released "free to air", to local and regional media and has also been broadcast in the US, the UK and elsewhere via the BBC, CNN and other organisations. The group's approach is to use targeted distribution in mainstream media and also post material on specific YouTube channels such as The Human Rights Channel. The content is sometimes posted anonymously, and supporters are encouraged to tweet links and post them through the social-media news distributor Storyful. The organisation has also started using Google and Facebook ads and to produce content to directly target specific issues. A recent project, recorded openly, was a short film that aims to end the practice of female genital mutilation (FGM). One woman describes how she used to wield a razor on young girls. She is now an anti- FGM campaigner. Videre's local partners have been taking the film around villages where Yakobovich says it has been having a significant impact in combating the practice. Eddie started work at the regional office last year. On his first day he watched footage of a man whose testicles had been smashed with a hammer. Videre would not release the footage. "We call that kind of extreme violence pornography," says Eddie. "We don't want it in the media. The ethos is not to shock but to effect change and we try to avoid the usual African stereotypes, the diet of violence." Eddie jokes that, when he applied for the job, Yakobovich repeatedly lied about the true nature of the work. The vague explanations that he was offered made it seem suspicious. "My parents thought they were after my kidneys," he says. Now Eddie "lies profusely", arranging hotels for couriers and others, always booking in false names and paying cash. In the charity's office in an neutral African country, Videre staffers sift operatives' covertly filmed footageLiam Sharp The same evening, Yakobovich and Carlos are back in the 4x4, tired following their long day and flights. They negotiate their way across the city to meet the researchers who have recently arrived from the neighbouring country. Two have come on the 18-hour bus ride and a third, known as The Chairman, has flown as he is the head of the network. Carlos has bought them each a chicken piri piri takeaway dinner with bottles of water and Coke. We meet at a neutral hotel -- not where they're staying, not where Wired is staying. A room has been hired which turns out to be somewhat larger than needed, as if for a banquet, so we gather at one end of the long table and Yakobovich puts some music on to prevent the conversation being overheard or eavesdropped: Hunky Dory by David Bowie. Carlos shows the three men his new cameras. They appear underwhelmed by his efforts. One model is a rubber-moulded base on to which a flag or other image can be added. But it is not the kind of thing that could be worn in the terror state. It would stand out. Two of the men are in their thirties and one is in his twenties. All three have wives and children and face grave risks in collecting and managing the material and their networks: they have been spooked by the recent arrest. The Chairman tells how, when a researcher was caught filming at a rally, he was beaten and issued with death threats if he failed to disclose his contacts. "When the manager of the man's network came on his monthly visit to collect the footage, he too was arrested," he says. "It was terrible, they held him for days without food, they beat him badly and then took him to a dam where they threw him in and left him, so he expected to drown. They pulled him out and said, OK, now talk, and he did give some information." Videre used lawyers and local fixers to obtain his release. "He was very shaken and in pain -- he felt bad about giving the information. But we said it was OK, it was better to give some information. He had a wife and children, and I reassured them as best I could when he went missing. They are brave people -- but the risks are there." The Chairman knows that, like Carlos, the security forces are aware of his identity if not his actual name. He faces arrest too, but says he is not afraid. "I haven't been caught yet and I pray it may never happen, I take every precaution, but if it comes I am ready for them," he says. "The camera is perfect for us. I believe it is the only way to achieve democratic change in the country. We do it with passion and understanding of the risks. I am ready," he says. The younger man has just had a child. He gave it a name in tribute to Carlos. In spite of his youth, Carlos is like a father figure to many of the researchers. He says many have named babies in his honour. That's just one of the reasons he cares so much about his work and about the people. As Videre embarks on a fund-raising campaign in the hope of expanding its work, the personal cost to Carlos remains high, not least to his marriage, and could go higher if he is ever arrested. Finally, he and Yakobovich leave the meeting with the researchers and head back to their hotel knowing that there is still much work to be done. Is it worth it? "Yes," Carlos says. "But I couldn't live like this forever." David James Smith is a writer for The Sunday Times Magazine and was Feature Writer of the Year at the British Press Awards 2012 -- Liberationtech is a public list whose archives are searchable on Google. Violations of list guidelines will get you moderated: https://mailman.stanford.edu/mailman/listinfo/liberationtech. Unsubscribe, change to digest, or change password by emailing moderator at companys(a)stanford.edu. ----- End forwarded message ----- -- Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org ______________________________________________________________ ICBM: 48.07100, 11.36820 http://ativel.com http://postbiota.org AC894EC5: 38A5 5F46 A4FF 59B8 336B 47EE F46E 3489 AC89 4EC5

1 0

open source drone autopilot
by Eugen Leitl 29 Aug '13

29 Aug '13

http://paparazzi.enac.fr/wiki/Lisa/S Lisa/S Lisa/S is a very small general purpose autopilot. The main goal of creating an autopilot of minimal size and weight, while providing a lot of functionality is achieved: Size: 20mm x 20mm x 5mm (0.787" x 0.787" x 0.197") Weight: 2.8g (0.1oz) Features 72MHz 32bit ARM Cortex M3 MCU with 16KB RAM and 512KB Flash Combined 3 Axis Gyroscope and 3 Axis Accelerometer 3 Axis Magnetometer Barometer (Altimeter) Onboard U-Blox GPS Pads to simply connect a Superbit CYRF RC and telemetry module Switching buck/boost converter allowing wide range of power input making it perfect and stable for operation from a 1S LiPO cell. 2 MOSFET switches connected to PWM output channels 6 PWM (servo) outputs 1 debug UART port 1 CAN interface 1 Bind/Boot tact switch SWD programming/debugging interface Size: 20mm x 20mm x 5mm (0.787" x 0.787" x 0.197") Weight: 2.8g (0.1oz) Pictures So if you are ready to make your tiny plane fly autonomously,you can already order one here.

1 0

Running in overlay circles [was: Why_can't_email_be_secure]
by grarpamp 29 Aug '13

29 Aug '13

On 8/26/13, rysiek <rysiek(a)hackerspace.pl> wrote: > It's a seemingly unsolvable conundrum: > - start with a clean slate and create a new, "perfect" solution; > - start with something people already use and improve it as much as > possible. > > The former approach has the risk of the solution not being adopted; the > latter > -- of the new solution not being good enough due to technicalities of the > solution it is based on. > > But maybe it could be possible to get the best of both worlds? > > Had a new solution been created in a way that is usable via existing mail > clients (e.g. implementing IMAP for message retrieval and SMTP for message > submission) while designing and implementing a completely new way of > comminicating server-to-server -- it might achieve just that. When you cleanslate things you are not held back by the past. Napster, bittorrent, icq... all completely new and instant mass appeal, because they did something that people wanted. That overrode every other consideration the user had, including... now hang on, I know this will be hard for some to believe.... downloading and installing the app and actually learning how to use it. These days, there is a want for secure messaging. Thanks to recent news... I'm actually taking questions from morons off the street that now want to 'send secret messages'. I don't have time so the standard answer is usually 'read and pick something from prism-break.org.' There are already cleanslate systems cryptographically secure against content and internal addressing snooping. The resistance to global passive/active adversaries from connecting the realworld IP talkers needs work. And to truly replace traditional email (especially in the business world) you will need a community of powerful messaging clients... lots of spec decisions to be made there... lots of traction with existing thunderbird, mutt, etc UI/handling frontends. But can you save that and swap out their legacy smtp/imap network semantics. Then you have the userspace key management for end2end message security to work on as well. All of this is interconnected too... once you start designing a strong messaging system, it begins to look like a general purpose transport, possibly one with parameterized options. Then you start thinking how to plug other apps into it. So you're back to looking like another I2P, Tor, GnuNet, Phantom, Freenet, AnoNet, etc... lots of the same stuff under the hood. Will there ever be a generic, possibly modular, overlay to come along and handle it all? Or are we just running in overlay circles?

1 0

Tin Can
by Frederic Jacobs 28 Aug '13

28 Aug '13

Mozilla released something that looks pretty good. Haven’t looked at the security yet. It’s peer to peer video that works in the browser with WebRTC and uses Persona to sign in. http://tincan.im/

2 1

Metadata anonymization through time delayed email messaging.
by Jeff Scofield 28 Aug '13

28 Aug '13

We know that with or without data content analysis of actual email messages, lots of information can be inferred through various forms of metadata collection. Given this reality the question becomes, what can be done? One strategy might be to consider the adoption of a time delayed email system. The reason why the use of such a mechanism to allow someone the ability to write an email, and then have it sent off at a specified (or randomly generated unspecified) date is useful for multiple reasons. If a program could be coded in a way which could delay the actual transmission of data in such a manner that the original time of creation was adequately masked, it could hamper nefarious metadata collection of time-stamping and possibly geo-locating of user information. For example: A person walks into a computer café at 10am and sets an email to send at around 4am the following morning (via cloud or machine). The data gets sent at 4am when the building is empty. No CCTV photos/cameras are able to document who sent the message because the computer café is unoccupied at 4am. The software is designed in such a fashion that it is nearly impossible to unmask the original time when the message was instructed to send, thus hiding the metadata associated with time-stamping, and thus hiding the true identity of the computer user at the café at 10am the previous day. Any and all feed back regarding this idea is welcome.

8 8

Geotemporal Public Key Distribution
by Rich Jones 27 Aug '13

27 Aug '13

This is a small, unfinished idea I had, but I'd be interested in hearing any feedback anybody here might have to offer. Normally we talk about cryptography to secure communications, but this is an idea rather about verifying the authenticity of media. [Quick backround: OpenWatch <https://openwatch.net> is a global citizen media network using mobile phones as the basis for a free worldwide press. We care very much about the authenticity of citizen media, and have designed some systems <https://github.com/Miserlou/CitizenMediaNotary>which attempt to improve the verifiability of citizen media.] The problem is that sometimes media artifacts are presented as a record of a current event, when in fact they from different events. An example of this was when images of a marathon race in Istanbul were presented as images<http://twitchy.com/2013/06/01/debunked-photo-of-occupygezi-crowds-crossing-…>of the recent Occupy Gezi protests. Now, imagine the globe divided into a grid coordinate system, say 100,000 units (or perhaps 232, if IP rather than physical address is to be used). Based on their physical location, reporters can contact a server and are assigned a key with which to sign or encrypt their media to. This then ties a media object to a physical space. This can be further improved to include both time and space by dividing a space-day into a number of units, suppose 1440, such that different keys would be handed out at different times of the day, thus further tying a document to a moment in time as well. Does anybody know if any systems like this have ever been discussed or designed in the past? I suppose this is somewhat similar to the RSA-keyfob system, although this allows for anonymous access without pre-arrangement as well. R

3 7