The only reference I know for Künneth theorems in this generality are SGA4 and SGA4.5. Specifically, SGA4 has theorems for étale cohomology with proper support (which hold in ridiculous generality), but SGA4.5's "Théorèmes de finitude en cohomologie $l$-adique" allows you to get the same results for étale cohomology, provided that the schemes are of finite type over a field (no other assumptions are needed!). The basic Künneth theorem itself is given as Corollaire 1.11 in that exposé. It is stated for schemes of finite type over a separably closed field, but if I'm not mistaken the proof works over any field whatsoever if you replace global sections by pushforwards to the étale topos of the base field. So this only gives you an equivalence between chain complexes with an action of the Galois group. The actual "étale cochains" are the invariants of those, and I don't know how to compute the invariants of a tensor product. But at least this reduces the problem to one in group cohomology.

**ADDED:** Here's a different approach. I think it may be true that for $X$ and $Y$ schemes of finite type over a field $k$, the cohomology of say $\mathbb{Z}/l^n$ over $X\times_kY$ can be computed as the $\mathbb{Z}/l^n$-cohomology of the homotopy pullback of étale homotopy types $Et(X)\times_{Et(k)}Et(Y)$. My argument is currently very **WRONG** though. <del>The idea is that (1) $Et(X)$ should be the homotopy fixed points of $Et(\bar X)$ (where $\bar X=X\times_k\bar k$), (2) the result is obviously true over $\bar k$ (by the Künneth theorem), and (3) homotopy fixed points commute with homotopy pullbacks.The usefulness of this is limited since it is not easy to compute the cohomology of a homotopy pullback, but this would give a "closed formula" answer only in terms of $X$, $Y$, and $k$.</del>

**ADDED 2**: I gave this a bit more thought and it obviously doesn't work. $Et(X)$ is the homotopy *orbits* of $Et(\bar X)$, and again I don't know how to compute the homotopy orbits of a pullback. The pullback formula is still true if $Y$ is proper and smooth over $k$. In this case you have a fiber sequence of $l$-completed étale homotopy types:

$$Et(\bar Y)\to Et(X\times_kY)\to Et(X)$$

which you can compare with the fiber sequence

$$Et(\bar Y)\to Et(X)\times_{Et(k)}Et(Y)\to Et(X)$$

so that $Et(X\times_kY)$ and $Et(X)\times_{Et(k)}Et(Y)$ are $\mathbb{Z}/l^n$-cohomologically equivalent. These fiber sequences are established in [this paper][1] by Friedlander (Corollary 4.8). I wonder if the properness assumption can be removed using SGA 4.5.

**ADDED 3:** OK, I'm pretty sure the above fiber sequence argument will work for any $X$ and $Y$ of finite type over a field. The only reason Friedlander considers proper and smooth maps is to apply a corollary of the proper/smooth base change theorems from SGA4, exposé XVI, which I think works without that assumption when over a field, thanks to SGA4.5. I need this result myself so I will try to check it thoroughly.


  [1]: http://archive.numdam.org/ARCHIVE/PMIHES/PMIHES_1973__42_/PMIHES_1973__42__5_0/PMIHES_1973__42__5_0.pdf