For an approach that doesn't use any kind of Kunneth principle and is amenable, once you've established the basics, for "easy" verification of formulae consult Iversen's discussion in his book "Cohomology of Sheaves". This treatment is not entirely rigorous but with some thought you can catch all the subtleties and see things work the way they should.

The essential idea is that $D(X)$ models $\mathsf{Ext}$ cohomology classes, in $D(A,B[n])\cong\mathsf{Ext}^n_k(A,B)$ where $A,B$ are $k$-sheaves, $k$ a commutative ring, and we have various canonical isomorphisms:

- $\mathsf{Ext}^n_k(\underline{k},\mathscr{F})\cong\mathcal{H}^k(X;\mathscr{F})$
- $\mathsf{Ext}^n_k(\underline{k}_A,\mathscr{F})\cong\mathcal{H}^k_A(X;\mathscr{F})$ for
**closed** $A\subseteq X$
- $\mathsf{Ext}^n_k(\underline{k}_U,\mathscr{F})\cong\mathcal{H}^k(U;\mathscr{F}|_U)$ where $U\subseteq X$ is
*open*
- $\mathsf{Ext}^n_k(\underline{k}_W,\mathscr{F})\cong\mathcal{H}^k_W(U;\mathscr{F}|_U)$ where $W\subseteq X$ is locally closed, equal to $A\cap U$ for some closed $A$, open $U$

Here all extension modules are taken from the category of $k$-sheaves and $\underline{k}$ refers to the constant sheaf with coefficients in $k$ over some base space, $X,A,U,W$ respectively, and the subscript indicates we pushforward along the $!$ morphism. So $\underline{k}_Y$, for $Y\subseteq X$ and $j:Y\hookrightarrow X$ the inclusion, is the sheaf $j_!\underline{k}$ where $\underline{k}$ is the constant sheaf with coefficients in $k$ on the space $Y$.

However, $D(X)$ is not well behaved with respect to tensor products so you can consider the intermediate derived category $G^+(X)$ which is the homotopy category of bounded below complexes localised at pointwise homotopy equivalences. Maybe you can help me out and explain whether or not this is locally small. Anyway, since $(\mathscr{F}\otimes_k\mathscr{G})_x\cong\mathscr{F}_x\otimes_k\mathscr{G}_x$, the ordinary tensor product descends to a functor on $G^+$ and Iversen shows this is good enough for the $\mathsf{Ext}$ computations and combining cohomology classes in tensor product, apropos the isomorphisms I mention above. We can verify formulas in the cup product just by chasing commutative diagrams in $G^+$ which is nice, but there are lurking subtleties in whether Iversen's commutative diagrams really represent what they are claimed to (which is true, but requires additional effort to fully check).

Whether this agrees with the Cech cup product I don't yet know since I haven't thoroughly reviewed Godement's treatment of that. However Iversen offers a very easy proof of uniqueness of the cup product; you can calculate using essentially any resolution of $\underline{k}$ of choice which has a map of complexes $C\otimes_k C\to C$ lying over $k\otimes k\to k$. This is the final theorem of the subsection.