Author: Michael Greenberg

Twitter bots and OAuth

SoftwareLeave a comment

I’m working on a Twitter bot, and I ran up against something very annoying: apps need to be on an account with a mobile phone number. I have just one mobile phone, and it’s already tied to my real Twitter account. Rather than finding a way to get another mobile number, I had the bot authorize my app using Twitter’s OAuth API. Here’s how to do it.

Step one: collect your API keys. There’s a consumer key and a consumer secret, both available from your app’s page at apps.twitter.com. Never commit these to a repository or post them anywhere. I put them in a special file that I tell git to ignore, keys.py.

Step two: collect OAuth tokens. The key trick here is to collect tokens that are permanently good, using the out-of-band (OOB) PIN method. To actually send the requests, I used the requests-oauthlib library for Python. Here’s how to do it:

from requests_oauthlib import OAuth1Session
from keys import *

twitter = OAuth1Session(consumer_key, consumer_secret) # loaded from keys.py!
twitter.params['oauth_callback'] = 'oob' # make sure we're in PIN mode
r = twitter.post('https://api.twitter.com/oauth/request_token')

At this point, r.text will tell you, HTTP request parameter style, your oauth_token and oauth_secret. Add these to your keys.py file and copy the oauth_token to the clipboard.

Step three: authorize the app. Fire up a web browser and log in to the bot’s account. Go to https://api.twitter.com/oauth/authorize?oauth_token=[whatever your oauth_token was]. You’ll get a PIN number. Add it to your keys.py file.

Step four: finalize the authorization.

from requests_oauthlib import OAuth1Session
from keys import *
twitter = OAuth1Session(consumer_key, consumer_secret)
twitter.params['oauth_verifier'] = pin
r = twitter.get('https://api.twitter.com/oauth/access_token?oauth_token=' + oauth_token)

Now r.text will give you a new oauth_token and oauth_token_secret. Save these—they’re OAuth access tokens, which are how you can actually make API calls.

Step five: check that it worked. Log in to the bot account, go to settings, and check the apps subheading—your app should appear. You can tweet programmatically, now:

from requests_oauthlib import OAuth1Session
from keys import *

twitter = OAuth1Session(consumer_key, consumer_secret, oauth_access_token, oauth_token_secret)
twitter.post('https://api.twitter.com/1.1/statuses/update.json?status=Testing.')

I would be lying if I said I was 100% confident that everything from here on out is easy, but it seems like these access tokens are all you need after PIN based authorization.

PHPEnkoder 1.13

Blog, SoftwareLeave a comment

I’ve resolved some E_NOTICE-level messages that were showing up when people set WP_DEBUG to true. Thanks to Rootside for pointing out this problem on the WordPress forums. As always, please let me know on the forums or via email if you run into any problems.

Cultural criticism and ‘tech’

BlogLeave a comment

As an academic computer scientist, I frequently interact with the world of ‘tech’, as embodied by Silicon Valley, startups, etc. Many of my friends—from college, from graduate school—work there. My younger brother works there. One of the things that has kept me out of that world is my wariness of its politics, ethics, and aesthetics. I was delighted, then, when I was introduced to Model View Culture, a venue for cultural criticism of tech, sensu lato. They cover a wide range:

I’m writing because other academics—the audience of this blog—might be interested. Many students coming out of the elite CS programs (my academic home for more than a decade) are going to end up working in the world MVC writes about. They’ll go as interns and then as employees. What is it like there?

But I’m also writing because MVC has been subjected to tremendous blowback. I’m not going to link to it, but it’s not hard to find. Silence is complicity, so: Model View Culture is writing smart things about hard problems. If you’d like to support them, just reading is a fine place to start… but of course money is good, too.

PLVNET

Networking, Presentations, Programming LanguagesLeave a comment

I’m really happy to be part of the first PLVNET, a workshop on the intersection of PL, verification, and networking. I have two abstracts up for discussion.

The first abstract, Temporal NetKAT, is about adding reasoning about packet histories to a network policy language like NetKAT. The work on this is moving along quite nicely (thanks in large part to Ryan Beckett!), and I’m looking forward to the conversations it will spark.

The second abstract, Type systems for SDN controllers, is about using type systems to statically guarantee the absence of errors in controller programs. Fancy new switches have tons of features, which can be tricky to operate—can we make sure that a controller doesn’t make any mistakes when it talks to a switch? Some things are easy, like making sure that the match/action rules are sent to tables that can handle them; some things are harder, like making sure the controller doesn’t fill up a switch’s tables. I think this kind of work is a nice complement to the NetKAT “whole policy” approach, a sort of OpenFlow 1.3+ version of VeriCon with slightly different goals.

Should be fun!

Space-Efficient Manifest Contracts at POPL 15

Papers, Programming LanguagesLeave a comment

I am delighted to announce that Space-Efficient Manifest Contracts will appear at POPL 2015 in Mumbai. Here’s the abstract:

The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program’s asymptotic space complexity. While space efficiency for gradual types—contracts mediating untyped and typed code—is well studied, sound space efficiency for manifest contracts—contracts that check stronger properties than simple types, e.g., “is a natural” instead of “is an integer”—remains an open problem.

We show how to achieve sound space efficiency for manifest contracts with strong predicate contracts. The essential trick is breaking the contract checking down into coercions: structured, blame-annotated lists of checks. By carefully preventing duplicate coercions from appearing, we can restore space efficiency while keeping the same observable behavior.

The conference version is a slightly cut down version of my submission, focusing on the main result: eidetic λH is a space-efficient manifest contract calculus with the same operational behavior as classic λH. More discussion and intermediate results—all in a unified framework for space efficiency—can be found in the technical report on the arXiv.

Contracts: first-order interlopers in a higher-order world

Blog, Papers, Programming LanguagesLeave a comment

Reading Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer‘s POPL 2012 paper The Ins and Outs of Gradual Type Inference, I ran across a quote that could well appear directly in my POPL 2015 paper, Space-Efficient Manifest Contracts:

The key insight is that … we must recursively deconstruct higher-order types down to their first-order parts, solve for those …, and then reconstruct the higher-order parts … . [Emphasis theirs]

Now, they’re deconstructing “flows” in their type inference and I’m deconstructing types themselves. They have to be careful about what’s known in the program and what isn’t, and I have to be careful about blame labels. But in both cases, a proper treatment of errors creates some asymmetries. And in both cases, the solution is to break everything down to the first-order checks, reconstructing a higher-order solution afterwards.

The “make it all first order” approach contrasts with subtyping approaches (like in Well Typed Programs Can’t Be Blamed and Threesomes, with and without blame). I think it’s worth pointing out that as we begin to consider blame, contract composition operators look less and less like meet operations and more like… something entirely different. Should contracts with blame inhabit some kind of skew lattice? Something else?

I highly recommend the Rastogi et al. paper, with one note: when they say kind, I think they mean “type shape” or “type skeleton”—not “kind” in the sense of classifying types and type constructors. Edited to add: also, how often does a type inference paper include a performance evaluation? Just delightful!

Scheduling the discussion order at PC meetings

SoftwareLeave a comment

I recently wrote a bit of code for scheduling the discussion order of PC meetings so as to minimize traffic in and out of the room due to conflicts of interest. Given some information that HotCRP happily generates, the code generates a schedule, which can be further turned into a handout and slides showing the current paper’s conflicts and the two upcoming papers.

If you’re interested in using or contributing, I’ve put the code up at mgree/conflict on github.

New and improved: Space-Efficient Manifest Contracts

Programming Languages, SubmissionsLeave a comment

I have a new and much improved draft of my work on Space-Efficient Manifest Contracts. Here’s the abstract:

The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program’s asymptotic space complexity. While space efficiency for gradual types—contracts mediating untyped and typed code—is well studied, sound space efficiency for manifest contracts—contracts that check stronger properties than simple types, e.g., “is a natural” instead of “is an integer”—remains an open problem.

We show how to achieve sound space efficiency for manifest contracts with strong predicate contracts. We define a framework for space efficiency, traversing the design space with three different space-efficient manifest calculi. Along the way, we examine the diverse correctness criteria for contract semantics; we conclude with a language whose contracts enjoy (galactically) bounded, sound space consumption—they are observationally equivalent to the standard, space-inefficient semantics.

Update: it was accepted to POPL’15!

Concurrent NetCore: From Policies to Pipelines

Networking, Programming Languages, SubmissionsLeave a comment

Cole Schlesinger, Dave Walker, and I submitted a paper to ICFP 2014. It’s called Concurrent NetCore: From Policies to Pipelines. Here’s the abstract:

In a Software-Defined Network (SDN), a central, computationally powerful controller manages a set of distributed, computationally simple switches. The controller computes a policy describing how each switch should route packets and populates packet-processing tables on each switch with rules to enact the routing policy. As network conditions change, the controller continues to add and remove rules from switches to adjust the policy as needed.

Recently, the SDN landscape has begun to change as several proposals for new, reconfigurable switching architectures, such as RMT and FlexPipe have emerged. These platforms provide switch programmers with many, flexible tables for storing packet-processing rules, and they offer programmers control over the packet fields that each table can analyze and act on. These reconfigurable switch architectures support a richer SDN model in which a switch configuration phase precedes the rule population phase. In the configuration phase, the controller sends the switch a graph describing the layout and capabilities of the packet processing tables it will require during the population phase. Armed with this foreknowledge, the switch can allocate its hardware (or software) resources more efficiently.

We present a new, typed language, called Concurrent NetCore, for specifying routing policies and graphs of packet-processing tables. Concurrent NetCore includes features for specifying sequential, conditional and concurrent control-flow between packet- processing tables. We develop a fine-grained operational model for the language and prove this model coincides with a higher level denotational model when programs are well typed. We also prove several additional properties of well typed programs, including strong normalization and determinism. To illustrate the utility of the language, we develop linguistic models of both the RMT and FlexPipe architectures and we give a multi-pass compilation algorithm that translates graphs and routing policies to the RMT model.

A Balance of Power: Expressive, Analyzable Controller Programming

Blog, Networking, Papers, Programming Languages, Temporal Logic and VerificationLeave a comment

I just finished reading A Balance of Power: Expressive, Analyzable Controller Programming. It’s an interesting proposal, but I’m writing just to express my satisfaction with the following sentence:

When we hit expressive limits, however, our goal is not to keep growing this language—down that path lies sendmail.cf and other sulphurous designs—but to call out to full-language code.

‘Sulphurous’ indeed. Come for the nonmonotonic interpretation of learning, stay for the colorful prose.